doc(Order): miscellaneous typo fixes (leanprover-community#28651)

Co-authored-by: Harald Husum <harald.husum@intelecy.com>

Author: harahu

Mathlib/Order/CompactlyGenerated/Basic.lean

@@ -548,7 +548,7 @@ instance (priority := 100) isAtomistic_of_complementedLattice [ComplementedLatti
 
 /-!
 Now we will prove that a compactly generated modular atomistic lattice is a complemented lattice.
-Most explicitly, every element is the complement of a supremum of indepedendent atoms.
+Most explicitly, every element is the complement of a supremum of independent atoms.
 -/
 
 /-- In an atomic lattice, every element `b` has a complement of the form `sSup s` relative to a

Mathlib/Order/CompleteLattice/Finset.lean

@@ -68,7 +68,7 @@ theorem iUnion_eq_iUnion_finset (s : ι → Set α) : ⋃ i, s i = ⋃ t : Finse
 
 /-- Union of an indexed family of sets `s : ι → Set α` is equal to the union of the unions
 of finite subfamilies. This version works for `ι : Sort*`. See also `iUnion_eq_iUnion_finset` for
-a version that assumes `ι : Type*` but avoids `PLift`s in the right hand side. -/
+a version that assumes `ι : Type*` but avoids `PLift`s in the right-hand side. -/
 theorem iUnion_eq_iUnion_finset' (s : ι' → Set α) :
     ⋃ i, s i = ⋃ t : Finset (PLift ι'), ⋃ i ∈ t, s (PLift.down i) :=
   iSup_eq_iSup_finset' s

Mathlib/Order/Copy.lean

@@ -87,7 +87,7 @@ def GeneralizedHeytingAlgebra.copy (c : GeneralizedHeytingAlgebra α)
   himp := himp
   le_himp_iff _ _ _ := by simp [eq_le, eq_himp, eq_inf]
 
-/-- A function to create a provable equal copy of a generalised coheyting algebra
+/-- A function to create a provable equal copy of a generalised co-Heyting algebra
 with possibly different definitional equalities. -/
 def GeneralizedCoheytingAlgebra.copy (c : GeneralizedCoheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
@@ -121,7 +121,7 @@ def HeytingAlgebra.copy (c : HeytingAlgebra α)
   compl := compl
   himp_bot := by simp [eq_le, eq_himp, eq_bot, eq_compl]
 
-/-- A function to create a provable equal copy of a coheyting algebra
+/-- A function to create a provable equal copy of a co-Heyting algebra
 with possibly different definitional equalities. -/
 def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
@@ -140,7 +140,7 @@ def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
   hnot := hnot
   top_sdiff := by simp [eq_le, eq_sdiff, eq_top, eq_hnot]
 
-/-- A function to create a provable equal copy of a biheyting algebra
+/-- A function to create a provable equal copy of a bi-Heyting algebra
 with possibly different definitional equalities. -/
 def BiheytingAlgebra.copy (c : BiheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)

Mathlib/Order/DirectedInverseSystem.lean

@@ -47,7 +47,7 @@ to work.
 
 It is possible to circumvent the introduction of the `compat` condition using Zorn's lemma;
 if there is a chain of natural families (i.e. for any two families in the chain, one is an
-extension of the other) over lowersets (which are all of the form `Iic`, `Iio`, or `univ`),
+extension of the other) over lower sets (which are all of the form `Iic`, `Iio`, or `univ`),
 we can clearly take the union to get a natural family that extends them all. If a maximal
 natural family has domain `Iic i` or `Iio i` (`i` a limit), we already know how to extend it
 one step further to `Iic i⁺` or `Iic i` respectively, so it must be the case that the domain

Mathlib/Order/Disjointed.lean

@@ -293,7 +293,7 @@ section Nat
 /-!
 ### Functions on `ℕ`
 
-(See also `Mathlib/Algebra/Order/Disjointed.lean` for results with more algebra pre-requsisites.)
+(See also `Mathlib/Algebra/Order/Disjointed.lean` for results with more algebra pre-requisites.)
 -/
 
 variable [GeneralizedBooleanAlgebra α]

Mathlib/Order/GaloisConnection/Defs.lean

@@ -223,7 +223,7 @@ end GaloisConnection
 choice function, to give better definitional equalities when lifting order structures. Dual
 to `GaloisCoinsertion` -/
 structure GaloisInsertion {α β : Type*} [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
-  /-- A contructive choice function for images of `l`. -/
+  /-- A constructive choice function for images of `l`. -/
   choice : ∀ x : α, u (l x) ≤ x → β
   /-- The Galois connection associated to a Galois insertion. -/
   gc : GaloisConnection l u
@@ -289,7 +289,7 @@ end GaloisInsertion
 choice function, to give better definitional equalities when lifting order structures. Dual to
 `GaloisInsertion` -/
 structure GaloisCoinsertion [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
-  /-- A contructive choice function for images of `u`. -/
+  /-- A constructive choice function for images of `u`. -/
   choice : ∀ x : β, x ≤ l (u x) → α
   /-- The Galois connection associated to a Galois coinsertion. -/
   gc : GaloisConnection l u

Mathlib/Order/Heyting/Basic.lean

@@ -30,7 +30,7 @@ Heyting algebras are the order theoretic equivalent of cartesian-closed categori
 * `GeneralizedCoheytingAlgebra`: Co-Heyting algebra without a bottom element (nor complement).
 * `HeytingAlgebra`: Heyting algebra.
 * `CoheytingAlgebra`: Co-Heyting algebra.
-* `BiheytingAlgebra`: bi-Heyting algebra.
+* `BiheytingAlgebra`: Bi-Heyting algebra.
 
 ## References
 

Mathlib/Order/LatticeIntervals.lean

@@ -17,9 +17,9 @@ intervals, but more can be added easily along the same lines when needed.
 
 In the following, `*` can represent either `c`, `o`, or `i`.
   * `Set.Ic*.orderBot`
-  * `Set.Ii*.semillaticeInf`
+  * `Set.Ii*.semilatticeInf`
   * `Set.I*c.orderTop`
-  * `Set.I*c.semillaticeInf`
+  * `Set.I*c.semilatticeInf`
   * `Set.I**.lattice`
   * `Set.Iic.boundedOrder`, within an `OrderBot`
   * `Set.Ici.boundedOrder`, within an `OrderTop`

Mathlib/Order/README.md

@@ -6,7 +6,7 @@ This folder contains order theory in a broad sense.
 
 The basic order hierarchy is split across a series of subfolders that each depend on the previous:
 * `Order.Preorder` for preorders, partial orders, lattices, linear orders
-* `Order.BooleanAlgebra` for heyting/biheyting/coheyting/boolean algebras
+* `Order.BooleanAlgebra` for Heyting/bi-Heyting/co-Heyting/boolean algebras
 * `Order.CompleteLattice` for frames, coframes, complete lattices
 * `Order.ConditionallyCompleteLattice` for conditionally complete lattices
 * `Order.CompleteBooleanAlgebra` for complete boolean algebras

Mathlib/Order/SupClosed.lean

@@ -323,7 +323,7 @@ lemma finsetSup'_mem_supClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {
 
 lemma supClosure_min : s ⊆ t → SupClosed t → supClosure s ⊆ t := supClosure.closure_min
 
-/-- The semilatice generated by a finite set is finite. -/
+/-- The semilattice generated by a finite set is finite. -/
 protected lemma Set.Finite.supClosure (hs : s.Finite) : (supClosure s).Finite := by
   lift s to Finset α using hs
   classical
@@ -395,7 +395,7 @@ lemma finsetInf'_mem_infClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {
 
 lemma infClosure_min : s ⊆ t → InfClosed t → infClosure s ⊆ t := infClosure.closure_min
 
-/-- The semilatice generated by a finite set is finite. -/
+/-- The semilattice generated by a finite set is finite. -/
 protected lemma Set.Finite.infClosure (hs : s.Finite) : (infClosure s).Finite := by
   lift s to Finset α using hs
   classical