diff --git a/src/data/finsupp/lattice.lean b/src/data/finsupp/lattice.lean
index a6fdbf1b5b97e..8144dd6568635 100644
--- a/src/data/finsupp/lattice.lean
+++ b/src/data/finsupp/lattice.lean
@@ -88,29 +88,29 @@ begin
 end
 
 /-- The lattice of `finsupp`s to `ℕ` is order-isomorphic to that of `multiset`s.  -/
-def rel_iso_multiset :
-  (has_le.le : (α →₀ ℕ) → (α →₀ ℕ) → Prop) ≃r (has_le.le : (multiset α) → (multiset α) → Prop) :=
+def order_iso_multiset :
+  (α →₀ ℕ) ≃o multiset α :=
 ⟨finsupp.equiv_multiset, begin
   intros a b, unfold finsupp.equiv_multiset, dsimp,
   rw multiset.le_iff_count, simp only [finsupp.count_to_multiset], refl
 end ⟩
 
-@[simp] lemma rel_iso_multiset_apply {f : α →₀ ℕ} : rel_iso_multiset f = f.to_multiset := rfl
+@[simp] lemma order_iso_multiset_apply {f : α →₀ ℕ} : order_iso_multiset f = f.to_multiset := rfl
 
-@[simp] lemma rel_iso_multiset_symm_apply {s : multiset α} :
-  rel_iso_multiset.symm s = s.to_finsupp :=
-by { conv_rhs { rw ← (rel_iso.apply_symm_apply rel_iso_multiset) s}, simp }
+@[simp] lemma order_iso_multiset_symm_apply {s : multiset α} :
+  order_iso_multiset.symm s = s.to_finsupp :=
+by { conv_rhs { rw ← (rel_iso.apply_symm_apply order_iso_multiset) s}, simp }
 
 variable [partial_order β]
 
 /-- The order on `finsupp`s over a partial order embeds into the order on functions -/
-def rel_embedding_to_fun :
-  (has_le.le : (α →₀ β) → (α →₀ β) → Prop) ↪r (has_le.le : (α → β) → (α → β) → Prop) :=
+def order_embedding_to_fun :
+  (α →₀ β) ↪o (α → β) :=
 ⟨⟨λ (f : α →₀ β) (a : α), f a,  λ f g h, finsupp.ext (λ a, by { dsimp at h, rw h,} )⟩,
   λ a b, le_def⟩
 
-@[simp] lemma rel_embedding_to_fun_apply {f : α →₀ β} {a : α} :
-  rel_embedding_to_fun f a = f a := rfl
+@[simp] lemma order_embedding_to_fun_apply {f : α →₀ β} {a : α} :
+  order_embedding_to_fun f a = f a := rfl
 
 lemma monotone_to_fun : monotone (finsupp.to_fun : (α →₀ β) → (α → β)) := λ f g h a, le_def.1 h a
 
diff --git a/src/data/setoid/basic.lean b/src/data/setoid/basic.lean
index eb4c64e8c0a6c..8f1ce9b1d693b 100644
--- a/src/data/setoid/basic.lean
+++ b/src/data/setoid/basic.lean
@@ -317,8 +317,7 @@ open quotient
 
 /-- Given an equivalence relation r on α, the order-preserving bijection between the set of
     equivalence relations containing r and the equivalence relations on the quotient of α by r. -/
-def correspondence (r : setoid α) : ((≤) : {s // r ≤ s} → {s // r ≤ s} → Prop) ≃r
-  ((≤) : setoid (quotient r) → setoid (quotient r) → Prop) :=
+def correspondence (r : setoid α) : {s // r ≤ s} ≃o setoid (quotient r) :=
 { to_fun := λ s, map_of_surjective s.1 quotient.mk ((ker_mk_eq r).symm ▸ s.2) exists_rep,
   inv_fun := λ s, ⟨comap quotient.mk s, λ x y h, show s.rel ⟦x⟧ ⟦y⟧, by rw eq_rel.2 h⟩,
   left_inv := λ s, subtype.ext_iff_val.2 $ ext' $ λ _ _,
diff --git a/src/data/setoid/partition.lean b/src/data/setoid/partition.lean
index 9539268e822f0..b5120189338aa 100644
--- a/src/data/setoid/partition.lean
+++ b/src/data/setoid/partition.lean
@@ -176,7 +176,7 @@ variables (α)
 
 /-- The order-preserving bijection between equivalence relations and partitions of sets. -/
 def partition.rel_iso :
-  ((≤) : setoid α → setoid α → Prop) ≃r (@setoid.partition.partial_order α).le :=
+  setoid α ≃o subtype (@is_partition α) :=
 { to_fun := λ r, ⟨r.classes, empty_not_mem_classes, classes_eqv_classes⟩,
   inv_fun := λ x, mk_classes x.1 x.2.2,
   left_inv := mk_classes_classes,
diff --git a/src/group_theory/congruence.lean b/src/group_theory/congruence.lean
index c64bc1bac1dd5..3803e07ff07a6 100644
--- a/src/group_theory/congruence.lean
+++ b/src/group_theory/congruence.lean
@@ -516,8 +516,7 @@ open quotient
 @[to_additive "Given an additive congruence relation `c` on a type `M` with an addition,
 the order-preserving bijection between the set of additive congruence relations containing `c` and
 the additive congruence relations on the quotient of `M` by `c`."]
-def correspondence : ((≤) : {d // c ≤ d} → {d // c ≤ d} → Prop) ≃r
-  ((≤) : con c.quotient → con c.quotient → Prop) :=
+def correspondence : {d // c ≤ d} ≃o (con c.quotient) :=
 { to_fun := λ d, d.1.map_of_surjective coe _
     (by rw mul_ker_mk_eq; exact d.2) $ @exists_rep _ c.to_setoid,
   inv_fun := λ d, ⟨comap (coe : M → c.quotient) (λ x y, rfl) d, λ _ _ h,
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index f5ff05d3974ea..44110b7f26e2d 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -1432,8 +1432,7 @@ by rw [eq_bot_iff, ← map_le_map_iff' p.ker_subtype, map_bot, map_comap_subtype
 
 /-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N` -/
 def map_subtype.rel_iso :
-  ((≤) : submodule R p → submodule R p → Prop) ≃r
-  ((≤) : {p' : submodule R M // p' ≤ p} → {p' : submodule R M // p' ≤ p} → Prop) :=
+  submodule R p ≃o {p' : submodule R M // p' ≤ p} :=
 { to_fun    := λ p', ⟨map p.subtype p', map_subtype_le p _⟩,
   inv_fun   := λ q, comap p.subtype q,
   left_inv  := λ p', comap_map_eq_self $ by simp,
@@ -1442,18 +1441,12 @@ def map_subtype.rel_iso :
 
 /-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
 submodules of `M`. -/
-def map_subtype.le_rel_embedding :
-  ((≤) : submodule R p → submodule R p → Prop) ↪r ((≤) : submodule R M → submodule R M → Prop) :=
+def map_subtype.order_embedding :
+  submodule R p ↪o submodule R M :=
 (rel_iso.to_rel_embedding $ map_subtype.rel_iso p).trans (subtype.rel_embedding _ _)
 
 @[simp] lemma map_subtype_embedding_eq (p' : submodule R p) :
-  map_subtype.le_rel_embedding p p' = map p.subtype p' := rfl
-
-/-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
-submodules of `M`. -/
-def map_subtype.lt_rel_embedding :
-  ((<) : submodule R p → submodule R p → Prop) ↪r ((<) : submodule R M → submodule R M → Prop) :=
-(map_subtype.le_rel_embedding p).lt_embedding_of_le_embedding
+  map_subtype.order_embedding p p' = map p.subtype p' := rfl
 
 
 /-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
@@ -1528,8 +1521,7 @@ by rw [ker_liftq, le_antisymm h h', mkq_map_self]
 /-- The correspondence theorem for modules: there is an order isomorphism between submodules of the
 quotient of `M` by `p`, and submodules of `M` larger than `p`. -/
 def comap_mkq.rel_iso :
-  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ≃r
-  ((≤) : {p' : submodule R M // p ≤ p'} → {p' : submodule R M // p ≤ p'} → Prop) :=
+  submodule R p.quotient ≃o {p' : submodule R M // p ≤ p'} :=
 { to_fun    := λ p', ⟨comap p.mkq p', le_comap_mkq p _⟩,
   inv_fun   := λ q, map p.mkq q,
   left_inv  := λ p', map_comap_eq_self $ by simp,
@@ -1538,18 +1530,12 @@ def comap_mkq.rel_iso :
 
 /-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
 of `M`. -/
-def comap_mkq.le_rel_embedding :
-  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ↪r ((≤) : submodule R M → submodule R M → Prop) :=
+def comap_mkq.order_embedding :
+  submodule R p.quotient ↪o submodule R M :=
 (rel_iso.to_rel_embedding $ comap_mkq.rel_iso p).trans (subtype.rel_embedding _ _)
 
 @[simp] lemma comap_mkq_embedding_eq (p' : submodule R p.quotient) :
-  comap_mkq.le_rel_embedding p p' = comap p.mkq p' := rfl
-
-/-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
-of `M`. -/
-def comap_mkq.lt_rel_embedding :
-  ((<) : submodule R p.quotient → submodule R p.quotient → Prop) ↪r ((<) : submodule R M → submodule R M → Prop) :=
-(comap_mkq.le_rel_embedding p).lt_embedding_of_le_embedding
+  comap_mkq.order_embedding p p' = comap p.mkq p' := rfl
 
 end ring
 
diff --git a/src/order/basic.lean b/src/order/basic.lean
index 6fdc0b76c7b47..a249a231363b0 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -77,9 +77,9 @@ theorem linear_order.ext {α} {A B : linear_order α}
 by { haveI this := partial_order.ext H,
      casesI A, casesI B, injection this, congr' }
 
-/-- Given an order `R` on `β` and a function `f : α → β`,
-  the preimage order on `α` is defined by `x ≤ y ↔ f x ≤ f y`.
-  It is the unique order on `α` making `f` an order embedding
+/-- Given a relation `R` on `β` and a function `f : α → β`,
+  the preimage relation on `α` is defined by `x ≤ y ↔ f x ≤ f y`.
+  It is the unique relation on `α` making `f` a `rel_embedding`
   (assuming `f` is injective). -/
 @[simp] def order.preimage {α β} (f : α → β) (s : β → β → Prop) (x y : α) := s (f x) (f y)
 
diff --git a/src/order/galois_connection.lean b/src/order/galois_connection.lean
index 13f8bd694ac27..1cf73b9b81421 100644
--- a/src/order/galois_connection.lean
+++ b/src/order/galois_connection.lean
@@ -54,9 +54,9 @@ variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a a₁ a₂ :
 def galois_connection [preorder α] [preorder β] (l : α → β) (u : β → α) := ∀a b, l a ≤ b ↔ a ≤ u b
 
 /-- Makes a Galois connection from an order-preserving bijection. -/
-theorem rel_iso.to_galois_connection [preorder α] [preorder β] (ri : @rel_iso α β (≤) (≤)) :
-  galois_connection ri ri.symm :=
-λ b g, by rw [ri.map_rel_iff, rel_iso.apply_symm_apply]
+theorem order_iso.to_galois_connection [preorder α] [preorder β] (oi : α ≃o β) :
+  galois_connection oi oi.symm :=
+λ b g, by rw [oi.map_rel_iff, rel_iso.apply_symm_apply]
 
 namespace galois_connection
 
@@ -241,7 +241,7 @@ def galois_insertion.monotone_intro {α β : Type*} [preorder α] [preorder β]
   choice_eq := λ _ _, rfl }
 
 /-- Makes a Galois insertion from an order-preserving bijection. -/
-protected def rel_iso.to_galois_insertion [preorder α] [preorder β] (oi : @rel_iso α β (≤) (≤)) :
+protected def rel_iso.to_galois_insertion [preorder α] [preorder β] (oi : α ≃o β) :
 @galois_insertion α β _ _ (oi) (oi.symm) :=
 { choice := λ b h, oi b,
   gc := oi.to_galois_connection,
@@ -411,7 +411,7 @@ def galois_insertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Makes a Galois coinsertion from an order-preserving bijection. -/
-protected def rel_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : @rel_iso α β (≤) (≤)) :
+protected def rel_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : α ≃o β) :
 @galois_coinsertion α β _ _ (oi) (oi.symm) :=
 { choice := λ b h, oi.symm b,
   gc := oi.to_galois_connection,
diff --git a/src/order/ord_continuous.lean b/src/order/ord_continuous.lean
index baca60e2089a8..083a2bb27731b 100644
--- a/src/order/ord_continuous.lean
+++ b/src/order/ord_continuous.lean
@@ -91,23 +91,15 @@ by simp only [lt_iff_le_not_le, hf.le_iff h]
 
 variable (f)
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_le_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop) :=
+/-- Convert an injective left order continuous function to an order embedding. -/
+def to_order_embedding (hf : left_ord_continuous f) (h : injective f) :
+  α ↪o β :=
 ⟨⟨f, h⟩, λ x y, (hf.le_iff h).symm⟩
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_lt_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ((<) : α → α → Prop) ↪r ((<) : β → β → Prop) :=
-⟨⟨f, h⟩, λ x y, (hf.lt_iff h).symm⟩
-
 variable {f}
 
-@[simp] lemma coe_to_le_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_le_rel_embedding f h) = f := rfl
-
-@[simp] lemma coe_to_lt_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_lt_rel_embedding f h) = f := rfl
+@[simp] lemma coe_to_order_embedding (hf : left_ord_continuous f) (h : injective f) :
+  ⇑(hf.to_order_embedding f h) = f := rfl
 
 end semilattice_sup
 
@@ -194,23 +186,14 @@ hf.order_dual.lt_iff h
 
 variable (f)
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_le_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop) :=
+/-- Convert an injective left order continuous function to a `order_embedding`. -/
+def to_order_embedding (hf : right_ord_continuous f) (h : injective f) : α ↪o β :=
 ⟨⟨f, h⟩, λ x y, (hf.le_iff h).symm⟩
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_lt_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ((<) : α → α → Prop) ↪r ((<) : β → β → Prop) :=
-⟨⟨f, h⟩, λ x y, (hf.lt_iff h).symm⟩
-
 variable {f}
 
-@[simp] lemma coe_to_le_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_le_rel_embedding f h) = f := rfl
-
-@[simp] lemma coe_to_lt_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_lt_rel_embedding f h) = f := rfl
+@[simp] lemma coe_to_order_embedding (hf : right_ord_continuous f) (h : injective f) :
+  ⇑(hf.to_order_embedding f h) = f := rfl
 
 end semilattice_inf
 
@@ -249,11 +232,11 @@ end conditionally_complete_lattice
 
 end right_ord_continuous
 
-namespace rel_iso
+namespace order_iso
 
 section preorder
 
-variables [preorder α] [preorder β] (e : ((≤) : α → α → Prop) ≃r ((≤) : β → β → Prop))
+variables [preorder α] [preorder β] (e : α ≃o β)
   {s : set α} {x : α}
 
 protected lemma left_ord_continuous : left_ord_continuous e :=
@@ -262,9 +245,8 @@ protected lemma left_ord_continuous : left_ord_continuous e :=
   λ y hy, e.rel_symm_apply.1 $ (is_lub_le_iff hx).2 $ λ x' hx', e.rel_symm_apply.2 $ hy $
     mem_image_of_mem _ hx'⟩
 
-protected lemma right_ord_continuous : right_ord_continuous e :=
-@rel_iso.left_ord_continuous (order_dual α) (order_dual β) _ _ e.rsymm
+protected lemma right_ord_continuous : right_ord_continuous e := order_iso.left_ord_continuous e.osymm
 
 end preorder
 
-end rel_iso
+end order_iso
diff --git a/src/order/rel_iso.lean b/src/order/rel_iso.lean
index 41dcd71bd1ad0..eb42c88e4645a 100644
--- a/src/order/rel_iso.lean
+++ b/src/order/rel_iso.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import logic.embedding
 import order.rel_classes
+import data.fin
 
 open function
 
@@ -30,6 +31,13 @@ structure rel_embedding {α β : Type*} (r : α → α → Prop) (s : β → β
 
 infix ` ↪r `:25 := rel_embedding
 
+/-- An order embedding is an embedding `f : α ↪ β` such that `a ≤ b ↔ (f a) ≤ (f b)`.
+This definition is an abbreviation of `rel_embedding (≤) (≤)`. -/
+abbreviation order_embedding (α β : Type*) [has_le α] [has_le β] :=
+@rel_embedding α β (≤) (≤)
+
+infix ` ↪o `:25 := order_embedding
+
 /-- the induced relation on a subtype is an embedding under the natural inclusion. -/
 definition subtype.rel_embedding {X : Type*} (r : X → X → Prop) (p : X → Prop) :
 ((subtype.val : subtype p → X) ⁻¹'o r) ↪r r :=
@@ -67,11 +75,11 @@ theorem coe_fn_inj : ∀ ⦃e₁ e₂ : r ↪r s⦄, (e₁ : α → β) = e₂ 
 
 @[simp] theorem trans_apply (f : r ↪r s) (g : s ↪r t) (a : α) : (f.trans g) a = g (f a) := rfl
 
-/-- An relation embedding is also an relation embedding between dual relations. -/
+/-- a relation embedding is also a relation embedding between dual relations. -/
 def rsymm (f : r ↪r s) : swap r ↪r swap s :=
 ⟨f.to_embedding, λ a b, f.map_rel_iff⟩
 
-/-- If `f` is injective, then it is an relation embedding from the
+/-- If `f` is injective, then it is a relation embedding from the
   preimage relation of `s` to `s`. -/
 def preimage (f : α ↪ β) (s : β → β → Prop) : f ⁻¹'o s ↪r s := ⟨f, λ a b, iff.rfl⟩
 
@@ -114,7 +122,8 @@ protected theorem is_strict_order : ∀ (f : r ↪r s) [is_strict_order β s], i
 protected theorem is_trichotomous : ∀ (f : r ↪r s) [is_trichotomous β s], is_trichotomous α r
 | ⟨f, o⟩ ⟨H⟩ := ⟨λ a b, (or_congr o (or_congr f.inj'.eq_iff.symm o)).2 (H _ _)⟩
 
-protected theorem is_strict_total_order' : ∀ (f : r ↪r s) [is_strict_total_order' β s], is_strict_total_order' α r
+protected theorem is_strict_total_order' :
+  ∀ (f : r ↪r s) [is_strict_total_order' β s], is_strict_total_order' α r
 | f H := by exactI {..f.is_trichotomous, ..f.is_strict_order}
 
 protected theorem acc (f : r ↪r s) (a : α) : acc s (f a) → acc r a :=
@@ -131,7 +140,7 @@ protected theorem is_well_order : ∀ (f : r ↪r s) [is_well_order β s], is_we
 | f H := by exactI {wf := f.well_founded H.wf, ..f.is_strict_total_order'}
 
 /-- It suffices to prove `f` is monotone between strict relations
-  to show it is an relation embedding. -/
+  to show it is a relation embedding. -/
 def of_monotone [is_trichotomous α r] [is_asymm β s] (f : α → β)
   (H : ∀ a b, r a b → s (f a) (f b)) : r ↪r s :=
 begin
@@ -147,33 +156,71 @@ end
 @[simp] theorem of_monotone_coe [is_trichotomous α r] [is_asymm β s] (f : α → β) (H) :
   (@of_monotone _ _ r s _ _ f H : α → β) = f := rfl
 
--- If le is preserved by an relation embedding of preorders, then lt is too
-def lt_embedding_of_le_embedding [preorder α] [preorder β]
-  (f : ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop)) :
-(has_lt.lt : α → α → Prop) ↪r (has_lt.lt : β → β → Prop) :=
-{ map_rel_iff' := by intros; simp [lt_iff_le_not_le,f.map_rel_iff], .. f }
+/-- Embeddings of partial orders that preserve  -/
+def order_embedding_of_lt_embedding [partial_order α] [partial_order β]
+  (f : ((<) : α → α → Prop) ↪r ((<) : β → β → Prop)) :
+  α ↪o β :=
+{ map_rel_iff' := by { intros, simp [le_iff_lt_or_eq,f.map_rel_iff, f.injective] }, .. f }
 
 end rel_embedding
 
-/-- The inclusion map `fin n → ℕ` is an relation embedding. -/
-def fin.val.rel_embedding (n) : @rel_embedding (fin n) ℕ (<) (<) :=
+namespace order_embedding
+
+variables [preorder α] [preorder β] (f : α ↪o β)
+
+/-- lt is preserved by order embeddings of preorders -/
+def lt_embedding : ((<) : α → α → Prop) ↪r ((<) : β → β → Prop) :=
+{ map_rel_iff' := by intros; simp [lt_iff_le_not_le,f.map_rel_iff], .. f }
+
+@[simp] lemma lt_embedding_apply (x : α) : f.lt_embedding x = f x := rfl
+
+theorem map_le_iff : ∀ {a b}, a ≤ b ↔ (f a) ≤ (f b) := f.map_rel_iff'
+
+theorem map_lt_iff : ∀ {a b}, a < b ↔ (f a) < (f b) :=
+f.lt_embedding.map_rel_iff'
+
+protected theorem acc (a : α) : acc (<) (f a) → acc (<) a :=
+f.lt_embedding.acc a
+
+protected theorem well_founded :
+  well_founded ((<) : β → β → Prop) → well_founded ((<) : α → α → Prop) :=
+f.lt_embedding.well_founded
+
+protected theorem is_well_order [is_well_order β (<)] : is_well_order α (<) :=
+f.lt_embedding.is_well_order
+
+/-- An order embedding is also an order embedding between dual orders. -/
+def osymm : order_dual α ↪o order_dual β :=
+⟨f.to_embedding, λ a b, f.map_rel_iff⟩
+
+end order_embedding
+
+/-- The inclusion map `fin n → ℕ` is a relation embedding. -/
+def fin.val.rel_embedding (n) : (fin n) ↪o ℕ :=
 ⟨⟨fin.val, @fin.eq_of_veq _⟩, λ a b, iff.rfl⟩
 
-/-- The inclusion map `fin m → fin n` is an relation embedding. -/
-def fin_fin.rel_embedding {m n} (h : m ≤ n) : @rel_embedding (fin m) (fin n) (<) (<) :=
+/-- The inclusion map `fin m → fin n` is an order embedding. -/
+def fin_fin.rel_embedding {m n} (h : m ≤ n) : (fin m) ↪o (fin n) :=
 ⟨⟨λ ⟨x, h'⟩, ⟨x, lt_of_lt_of_le h' h⟩,
   λ ⟨a, _⟩ ⟨b, _⟩ h, by congr; injection h⟩,
   by intros; cases a; cases b; refl⟩
 
+/-- The ordering on `fin n` is a well order. -/
 instance fin.lt.is_well_order (n) : is_well_order (fin n) (<) :=
-(fin.val.rel_embedding _).is_well_order
+(fin.val.rel_embedding n).is_well_order
 
-/-- A relation isomorphism is an equivalence that is also an relation embedding. -/
+/-- A relation isomorphism is an equivalence that is also a relation embedding. -/
 structure rel_iso {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β :=
 (map_rel_iff' : ∀ {a b}, r a b ↔ s (to_equiv a) (to_equiv b))
 
 infix ` ≃r `:25 := rel_iso
 
+/-- An order isomorphism is an equivalence such that `a ≤ b ↔ (f a) ≤ (f b)`.
+This definition is an abbreviation of `rel_iso (≤) (≤)`. -/
+abbreviation order_iso (α β : Type*) [has_le α] [has_le β] := @rel_iso α β (≤) (≤)
+
+infix ` ≃o `:25 := order_iso
+
 namespace rel_iso
 
 /-- Convert an `rel_iso` to an `rel_embedding`. This function is also available as a coercion
@@ -332,34 +379,38 @@ rel_embedding.is_well_order (subrel.rel_embedding r p)
 
 end subrel
 
-/-- Restrict the codomain of an relation embedding -/
+/-- Restrict the codomain of a relation embedding -/
 def rel_embedding.cod_restrict (p : set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r subrel s p :=
 ⟨f.to_embedding.cod_restrict p H, f.map_rel_iff'⟩
 
 @[simp] theorem rel_embedding.cod_restrict_apply (p) (f : r ↪r s) (H a) :
   rel_embedding.cod_restrict p f H a = ⟨f a, H a⟩ := rfl
 
+  /-- An order isomorphism is also an order isomorphism between dual orders. -/
+def order_iso.osymm [preorder α] [preorder β] (f : α ≃o β) :
+  order_dual α ≃o order_dual β := ⟨f.to_equiv, λ _ _, f.map_rel_iff⟩
+
 section lattice_isos
 
-lemma rel_iso.map_bot [order_bot α] [order_bot β]
-  (f : ((≤) : α → α → Prop) ≃r ((≤) : β → β → Prop)) :
+lemma order_iso.map_bot [order_bot α] [order_bot β]
+  (f : α ≃o β) :
   f ⊥ = ⊥ :=
 by { rw [eq_bot_iff, ← f.apply_symm_apply ⊥, ← f.map_rel_iff], apply bot_le, }
 
 lemma rel_iso.map_top [order_top α] [order_top β]
-  (f : ((≤) : α → α → Prop) ≃r ((≤) : β → β → Prop)) :
+  (f : α ≃o β) :
   f ⊤ = ⊤ :=
 by { rw [eq_top_iff, ← f.apply_symm_apply ⊤, ← f.map_rel_iff], apply le_top, }
 
 variables {a₁ a₂ : α}
 
 lemma rel_embedding.map_inf_le [semilattice_inf α] [semilattice_inf β]
-  (f : ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop)) :
+  (f : α ↪o β) :
   f (a₁ ⊓ a₂) ≤ f a₁ ⊓ f a₂ :=
 by simp [← f.map_rel_iff]
 
 lemma rel_iso.map_inf [semilattice_inf α] [semilattice_inf β]
-  (f : ((≤) : α → α → Prop) ≃r ((≤) : β → β → Prop)) :
+  (f : α ≃o β) :
   f (a₁ ⊓ a₂) = f a₁ ⊓ f a₂ :=
 begin
   apply le_antisymm, { apply f.to_rel_embedding.map_inf_le },
@@ -368,13 +419,13 @@ begin
 end
 
 lemma rel_embedding.le_map_sup [semilattice_sup α] [semilattice_sup β]
-  (f : ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop)) :
+  (f : α ↪o β) :
   f a₁ ⊔ f a₂ ≤ f (a₁ ⊔ a₂) :=
 by simp [← f.map_rel_iff]
 
 
 lemma rel_iso.map_sup [semilattice_sup α] [semilattice_sup β]
-  (f : ((≤) : α → α → Prop) ≃r ((≤) : β → β → Prop)) :
+  (f : α ≃o β) :
   f (a₁ ⊔ a₂) = f a₁ ⊔ f a₂ :=
 begin
   apply le_antisymm, swap, { apply f.to_rel_embedding.le_map_sup },
diff --git a/src/order/semiconj_Sup.lean b/src/order/semiconj_Sup.lean
index 822fe4234e0c6..ed4cd01de2a43 100644
--- a/src/order/semiconj_Sup.lean
+++ b/src/order/semiconj_Sup.lean
@@ -67,8 +67,8 @@ semiconjugate to `fa` by `g'`.
 This is a version of Proposition 2.1 from [Étienne Ghys, Groupes d'homeomorphismes du cercle et
 cohomologie bornee][ghys87:groupes]. -/
 lemma semiconj.symm_adjoint [partial_order α] [preorder β]
-  {fa : ((≤) : α → α → Prop) ≃r ((≤) : α → α → Prop)}
-  {fb : ((≤) : β → β → Prop) ↪r ((≤) : β → β → Prop)} {g : α → β}
+  {fa : α ≃o α}
+  {fb : β ↪o β} {g : α → β}
   (h : function.semiconj g fa fb) {g' : β → α} (hg' : is_order_right_adjoint g g') :
   function.semiconj g' fb fa :=
 begin
@@ -80,7 +80,7 @@ end
 variable {G : Type*}
 
 lemma semiconj_of_is_lub [partial_order α] [group G]
-  (f₁ f₂ : G →* ((≤) : α → α → Prop) ≃r ((≤) : α → α → Prop)) {h : α → α}
+  (f₁ f₂ : G →* (α ≃o α)) {h : α → α}
   (H : ∀ x, is_lub (range (λ g', (f₁ g')⁻¹ (f₂ g' x))) (h x)) (g : G) :
   function.semiconj h (f₂ g) (f₁ g) :=
 begin
@@ -96,7 +96,7 @@ isomorphisms. Then the map `x ↦ ⨆ g : G, (f₁ g)⁻¹ (f₂ g x)` semiconju
 This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homeomorphismes du cercle et
 cohomologie bornee][ghys87:groupes]. -/
 lemma Sup_div_semiconj [complete_lattice α] [group G]
-  (f₁ f₂ : G →* ((≤) : α → α → Prop) ≃r ((≤) : α → α → Prop)) (g : G) :
+  (f₁ f₂ : G →* (α ≃o α)) (g : G) :
   function.semiconj (λ x, ⨆ g' : G, (f₁ g')⁻¹ (f₂ g' x)) (f₂ g) (f₁ g) :=
 semiconj_of_is_lub f₁ f₂ (λ x, is_lub_supr) _
 
@@ -107,7 +107,7 @@ Then the map `x ↦ Sup s(x)` semiconjugates each `f₁ g'` to `f₂ g'`.
 This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homeomorphismes du cercle et
 cohomologie bornee][ghys87:groupes]. -/
 lemma cSup_div_semiconj [conditionally_complete_lattice α] [group G]
-  (f₁ f₂ : G →* ((≤) : α → α → Prop) ≃r ((≤) : α → α → Prop))
+  (f₁ f₂ : G →* (α ≃o α))
   (hbdd : ∀ x, bdd_above (range $ λ g, (f₁ g)⁻¹ (f₂ g x))) (g : G) :
   function.semiconj (λ x, ⨆ g' : G, (f₁ g')⁻¹ (f₂ g' x)) (f₂ g) (f₁ g) :=
 semiconj_of_is_lub f₁ f₂ (λ x, is_lub_cSup (range_nonempty _) (hbdd x)) _
diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean
index bde457f121397..01b68539f2a02 100644
--- a/src/ring_theory/ideal/operations.lean
+++ b/src/ring_theory/ideal/operations.lean
@@ -651,8 +651,7 @@ lemma le_map_of_comap_le_of_surjective : comap f K ≤ I → K ≤ map f I :=
 
 /-- Correspondence theorem -/
 def rel_iso_of_surjective :
-  ((≤) : ideal S → ideal S → Prop) ≃r
-  ((≤) : { p : ideal R // comap f ⊥ ≤ p } → { p : ideal R // comap f ⊥ ≤ p } → Prop) :=
+  ideal S ≃o { p : ideal R // comap f ⊥ ≤ p } :=
 { to_fun := λ J, ⟨comap f J, comap_mono bot_le⟩,
   inv_fun := λ I, map f I.1,
   left_inv := λ J, map_comap_of_surjective f hf J,
@@ -662,14 +661,10 @@ def rel_iso_of_surjective :
   map_rel_iff' := λ I1 I2, ⟨comap_mono, λ H, map_comap_of_surjective f hf I1 ▸
     map_comap_of_surjective f hf I2 ▸ map_mono H⟩ }
 
-def le_rel_embedding_of_surjective :
-  ((≤) : ideal S → ideal S → Prop) ↪r ((≤) : ideal R → ideal R → Prop) :=
+/-- The map on ideals induced by a surjective map preserves inclusion. -/
+def order_embedding_of_surjective : ideal S ↪o ideal R :=
 (rel_iso_of_surjective f hf).to_rel_embedding.trans (subtype.rel_embedding _ _)
 
-def lt_rel_embedding_of_surjective :
-  ((<) : ideal S → ideal S → Prop) ↪r ((<) : ideal R → ideal R → Prop) :=
-(le_rel_embedding_of_surjective f hf).lt_embedding_of_le_embedding
-
 theorem map_eq_top_or_is_maximal_of_surjective (H : is_maximal I) :
   (map f I) = ⊤ ∨ is_maximal (map f I) :=
 begin
@@ -715,8 +710,7 @@ include hf
 open function
 
 /-- Special case of the correspondence theorem for isomorphic rings -/
-def rel_iso_of_bijective :
-  ((≤) : ideal S → ideal S → Prop) ≃r ((≤) : ideal R → ideal R → Prop):=
+def rel_iso_of_bijective : ideal S ≃o ideal R :=
 { to_fun := comap f,
   inv_fun := map f,
   left_inv := (rel_iso_of_surjective f hf.right).left_inv,
diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean
index 77822a4065924..05b5712152016 100644
--- a/src/ring_theory/localization.lean
+++ b/src/ring_theory/localization.lean
@@ -715,9 +715,8 @@ end
 
 /-- If `S` is the localization of `R` at a submonoid, the ordering of ideals of `S` is
 embedded in the ordering of ideals of `R`. -/
-def le_rel_embedding :
-  ((≤) : ideal S → ideal S → Prop) ↪r
-  ((≤) : ideal R → ideal R → Prop) :=
+def order_embedding :
+  ideal S ↪o ideal R :=
 { to_fun := λ J, ideal.comap f.to_map J,
   inj'   := function.left_inverse.injective f.map_comap,
   map_rel_iff'   := λ J₁ J₂, ⟨ideal.comap_mono, λ hJ,
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 39de7664d00f5..9a3d09a1aa7cf 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -382,16 +382,14 @@ theorem is_noetherian_of_submodule_of_noetherian (R M) [ring R] [add_comm_group
   (N : submodule R M) (h : is_noetherian R M) : is_noetherian R N :=
 begin
   rw is_noetherian_iff_well_founded at h ⊢,
-  convert rel_embedding.well_founded (rel_embedding.rsymm
-    (submodule.map_subtype.lt_rel_embedding N)) h
+  exact order_embedding.well_founded (submodule.map_subtype.order_embedding N).osymm h,
 end
 
 theorem is_noetherian_of_quotient_of_noetherian (R) [ring R] (M) [add_comm_group M] [module R M]
   (N : submodule R M) (h : is_noetherian R M) : is_noetherian R N.quotient :=
 begin
   rw is_noetherian_iff_well_founded at h ⊢,
-  convert rel_embedding.well_founded (rel_embedding.rsymm
-    (submodule.comap_mkq.lt_rel_embedding N)) h
+  exact order_embedding.well_founded (submodule.comap_mkq.order_embedding N).osymm h,
 end
 
 theorem is_noetherian_of_fg_of_noetherian {R M} [ring R] [add_comm_group M] [module R M]
@@ -435,10 +433,8 @@ theorem is_noetherian_ring_of_surjective (R) [comm_ring R] (S) [comm_ring S]
   (f : R →+* S) (hf : function.surjective f)
   [H : is_noetherian_ring R] : is_noetherian_ring S :=
 begin
-  unfold is_noetherian_ring at H ⊢,
-  rw is_noetherian_iff_well_founded at H ⊢,
-  convert rel_embedding.well_founded (rel_embedding.rsymm
-    (ideal.lt_rel_embedding_of_surjective f hf)) H
+  rw [is_noetherian_ring, is_noetherian_iff_well_founded] at H ⊢,
+  exact order_embedding.well_founded (ideal.order_embedding_of_surjective f hf).osymm H,
 end
 
 instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R →+* S)
diff --git a/src/set_theory/cardinal_ordinal.lean b/src/set_theory/cardinal_ordinal.lean
index 7adcc08b5f708..f8dc085297653 100644
--- a/src/set_theory/cardinal_ordinal.lean
+++ b/src/set_theory/cardinal_ordinal.lean
@@ -62,7 +62,7 @@ end
   For the basic function version, see `aleph_idx`.
   For an upgraded version stating that the range is everything, see `aleph_idx.rel_iso`. -/
 def aleph_idx.initial_seg : @initial_seg cardinal ordinal (<) (<) :=
-@rel_embedding.collapse cardinal ordinal (<) (<) _ cardinal.ord.rel_embedding
+@rel_embedding.collapse cardinal ordinal (<) (<) _ cardinal.ord.order_embedding.lt_embedding
 
 /-- The `aleph'` index function, which gives the ordinal index of a cardinal.
   (The `aleph'` part is because unlike `aleph` this counts also the
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index 8d8e418281f5a..0fe69951d39ef 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -1111,7 +1111,7 @@ namespace cardinal
 open ordinal
 
 /-- The ordinal corresponding to a cardinal `c` is the least ordinal
-  whose cardinal is `c`. For the order-embedding version, see `ord.rel_embedding`. -/
+  whose cardinal is `c`. For the order-embedding version, see `ord.order_embedding`. -/
 def ord (c : cardinal) : ordinal :=
 begin
   let ι := λ α, {r // is_well_order α r},
@@ -1212,11 +1212,12 @@ by { intros c c' h, rw [←card_ord c, ←card_ord c', h] }
 /-- The ordinal corresponding to a cardinal `c` is the least ordinal
   whose cardinal is `c`. This is the order-embedding version. For the regular function, see `ord`.
 -/
-def ord.rel_embedding : @rel_embedding cardinal ordinal (<) (<) :=
-rel_embedding.of_monotone cardinal.ord $ λ a b, cardinal.ord_lt_ord.2
+def ord.order_embedding : cardinal ↪o ordinal :=
+rel_embedding.order_embedding_of_lt_embedding
+  (rel_embedding.of_monotone cardinal.ord $ λ a b, cardinal.ord_lt_ord.2)
 
-@[simp] theorem ord.rel_embedding_coe :
-  (ord.rel_embedding : cardinal → ordinal) = ord := rfl
+@[simp] theorem ord.order_embedding_coe :
+  (ord.order_embedding : cardinal → ordinal) = ord := rfl
 
 /-- The cardinal `univ` is the cardinality of ordinal `univ`, or
   equivalently the cardinal of `ordinal.{u}`, or `cardinal.{u}`,