chore(init/algebra/order): typo

Thanks to @fpvandoorn for proof-reading!

doc/changes.md

@@ -107,7 +107,7 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
   most things that were once imported by this are now imported by default.
 
 * The type classes for orders have been refactored to combine both the `(<)`
-  and `(≤)` operations.  The new classes are `pre_order`, `partial_order`, and
+  and `(≤)` operations.  The new classes are `preorder`, `partial_order`, and
   `linear_order`.  The `partial_order` class corresponds to `weak_order`,
   `strict_order`, `order_pair`, and `strong_order_pair`.  The `linear_order`
   class corresponds to `linear_order_pair`, and `linear_strong_order_pair`.

library/init/algebra/order.lean

@@ -15,43 +15,43 @@ universe u
 variables {α : Type u}
 
 set_option auto_param.check_exists false
-class pre_order (α : Type u) extends has_le α, has_lt α :=
+class preorder (α : Type u) extends has_le α, has_lt α :=
 (le_refl : ∀ a : α, a ≤ a)
 (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
 (lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
 (lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)
 
-class partial_order (α : Type u) extends pre_order α :=
+class partial_order (α : Type u) extends preorder α :=
 (le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
 
 class linear_order (α : Type u) extends partial_order α :=
 (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)
 
-@[refl] lemma le_refl [pre_order α] : ∀ a : α, a ≤ a :=
-pre_order.le_refl
+@[refl] lemma le_refl [preorder α] : ∀ a : α, a ≤ a :=
+preorder.le_refl
 
-@[trans] lemma le_trans [pre_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
-pre_order.le_trans
+@[trans] lemma le_trans [preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
+preorder.le_trans
 
-lemma lt_iff_le_not_le [pre_order α] : ∀ {a b : α}, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
-pre_order.lt_iff_le_not_le _
+lemma lt_iff_le_not_le [preorder α] : ∀ {a b : α}, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
+preorder.lt_iff_le_not_le _
 
-lemma lt_of_le_not_le [pre_order α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b
+lemma lt_of_le_not_le [preorder α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b
 | a b hab hba := lt_iff_le_not_le.mpr ⟨hab, hba⟩
 
-lemma le_not_le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a
+lemma le_not_le_of_lt [preorder α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a
 | a b hab := lt_iff_le_not_le.mp hab
 
 lemma le_antisymm [partial_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
 partial_order.le_antisymm
 
-lemma le_of_eq [pre_order α] {a b : α} : a = b → a ≤ b :=
+lemma le_of_eq [preorder α] {a b : α} : a = b → a ≤ b :=
 λ h, h ▸ le_refl a
 
 lemma le_antisymm_iff [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a :=
 ⟨λe, ⟨le_of_eq e, le_of_eq e.symm⟩, λ⟨h1, h2⟩, le_antisymm h1 h2⟩
 
-@[trans] lemma ge_trans [pre_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
+@[trans] lemma ge_trans [preorder α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
 λ a b c h₁ h₂, le_trans h₂ h₁
 
 lemma le_total [linear_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
@@ -63,15 +63,15 @@ or.resolve_left (le_total b a)
 lemma le_of_not_le [linear_order α] {a b : α} : ¬ a ≤ b → b ≤ a :=
 or.resolve_left (le_total a b)
 
-lemma lt_irrefl [pre_order α] : ∀ a : α, ¬ a < a
+lemma lt_irrefl [preorder α] : ∀ a : α, ¬ a < a
 | a haa := match le_not_le_of_lt haa with
   | ⟨h1, h2⟩ := false.rec _ (h2 h1)
   end
 
-lemma gt_irrefl [pre_order α] : ∀ a : α, ¬ a > a :=
+lemma gt_irrefl [preorder α] : ∀ a : α, ¬ a > a :=
 lt_irrefl
 
-@[trans] lemma lt_trans [pre_order α] : ∀ {a b c : α}, a < b → b < c → a < c
+@[trans] lemma lt_trans [preorder α] : ∀ {a b c : α}, a < b → b < c → a < c
 | a b c hab hbc :=
   match le_not_le_of_lt hab, le_not_le_of_lt hbc with
   | ⟨hab, hba⟩, ⟨hbc, hcb⟩ := lt_of_le_not_le (le_trans hab hbc) (λ hca, hcb (le_trans hca hab))
@@ -79,46 +79,46 @@ lt_irrefl
 
 def lt.trans := @lt_trans
 
-@[trans] lemma gt_trans [pre_order α] : ∀ {a b c : α}, a > b → b > c → a > c :=
+@[trans] lemma gt_trans [preorder α] : ∀ {a b c : α}, a > b → b > c → a > c :=
 λ a b c h₁ h₂, lt_trans h₂ h₁
 
 def gt.trans := @gt_trans
 
-lemma ne_of_lt [pre_order α] {a b : α} (h : a < b) : a ≠ b :=
+lemma ne_of_lt [preorder α] {a b : α} (h : a < b) : a ≠ b :=
 λ he, absurd h (he ▸ lt_irrefl a)
 
-lemma ne_of_gt [pre_order α] {a b : α} (h : a > b) : a ≠ b :=
+lemma ne_of_gt [preorder α] {a b : α} (h : a > b) : a ≠ b :=
 λ he, absurd h (he ▸ lt_irrefl a)
 
-lemma lt_asymm [pre_order α] {a b : α} (h : a < b) : ¬ b < a :=
+lemma lt_asymm [preorder α] {a b : α} (h : a < b) : ¬ b < a :=
 λ h1 : b < a, lt_irrefl a (lt_trans h h1)
 
 lemma not_lt_of_gt [linear_order α] {a b : α} (h : a > b) : ¬ a < b :=
 lt_asymm h
 
-lemma le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b
+lemma le_of_lt [preorder α] : ∀ {a b : α}, a < b → a ≤ b
 | a b hab := (le_not_le_of_lt hab).left
 
-@[trans] lemma lt_of_lt_of_le [pre_order α] : ∀ {a b c : α}, a < b → b ≤ c → a < c
+@[trans] lemma lt_of_lt_of_le [preorder α] : ∀ {a b c : α}, a < b → b ≤ c → a < c
 | a b c hab hbc :=
   let ⟨hab, hba⟩ := le_not_le_of_lt hab in
   lt_of_le_not_le (le_trans hab hbc) $ λ hca, hba (le_trans hbc hca)
 
-@[trans] lemma lt_of_le_of_lt [pre_order α] : ∀ {a b c : α}, a ≤ b → b < c → a < c
+@[trans] lemma lt_of_le_of_lt [preorder α] : ∀ {a b c : α}, a ≤ b → b < c → a < c
 | a b c hab hbc :=
   let ⟨hbc, hcb⟩ := le_not_le_of_lt hbc in
   lt_of_le_not_le (le_trans hab hbc) $ λ hca, hcb (le_trans hca hab)
 
-@[trans] lemma gt_of_gt_of_ge [pre_order α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
+@[trans] lemma gt_of_gt_of_ge [preorder α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
 lt_of_le_of_lt h₂ h₁
 
-@[trans] lemma gt_of_ge_of_gt [pre_order α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
+@[trans] lemma gt_of_ge_of_gt [preorder α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
 lt_of_lt_of_le h₂ h₁
 
-lemma not_le_of_gt [pre_order α] {a b : α} (h : a > b) : ¬ a ≤ b :=
+lemma not_le_of_gt [preorder α] {a b : α} (h : a > b) : ¬ a ≤ b :=
 (le_not_le_of_lt h).right
 
-lemma not_lt_of_ge [pre_order α] {a b : α} (h : a ≥ b) : ¬ a < b :=
+lemma not_lt_of_ge [preorder α] {a b : α} (h : a ≥ b) : ¬ a < b :=
 λ hab, not_le_of_gt hab h
 
 lemma lt_or_eq_of_le [partial_order α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b
@@ -176,7 +176,7 @@ match lt_trichotomy a b with
 | or.inr (or.inr hgt) := or.inr hgt
 end
 
-lemma le_of_eq_or_lt [pre_order α] {a b : α} (h : a = b ∨ a < b) : a ≤ b :=
+lemma le_of_eq_or_lt [preorder α] {a b : α} (h : a = b ∨ a < b) : a ≤ b :=
 or.elim h le_of_eq le_of_lt
 
 lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b :=
@@ -185,7 +185,7 @@ lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b
 lemma lt_iff_not_ge [linear_order α] (x y : α) : x < y ↔ ¬ x ≥ y :=
 ⟨not_le_of_gt, lt_of_not_ge⟩
 
-instance decidable_lt_of_decidable_le [pre_order α]
+instance decidable_lt_of_decidable_le [preorder α]
   [decidable_rel ((≤) : α → α → Prop)] :
   decidable_rel ((<) : α → α → Prop)
 | a b :=

tests/lean/run/order_defaults.lean

@@ -1,4 +1,4 @@
-example : pre_order unit := {
+example : preorder unit := {
     le := λ _ _, true,
     le_refl := λ _, trivial,
     le_trans := λ _ _ _ _ _, trivial,