doc(Order): fix typos (leanprover-community#37519)

Author: harahu

Mathlib/Order/Birkhoff.lean

@@ -29,7 +29,7 @@ If `α` is moreover a distributive lattice:
   elements.
 * `OrderEmbedding.birkhoffSet`, `OrderEmbedding.birkhoffFinset`: Order embedding of `α` into the
   powerset lattice of its irreducible elements.
-* `LatticeHom.birkhoffSet`, `LatticeHom.birkhoffFinet`: Same as the previous two, but bundled as
+* `LatticeHom.birkhoffSet`, `LatticeHom.birkhoffFinset`: Same as the previous two, but bundled as
   an injective lattice homomorphism.
 * `exists_birkhoff_representation`: `α` embeds into some powerset algebra. You should prefer using
   this over the explicit Birkhoff embedding because the Birkhoff embedding is littered with

Mathlib/Order/ConditionallyCompletePartialOrder/Defs.lean

@@ -63,7 +63,7 @@ class ConditionallyCompletePartialOrderSup (α : Type*)
   isLUB_csSup_of_directed :
     ∀ s, DirectedOn (· ≤ ·) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)
 
-/-- Conditionally complete partial orders (with suprema and infimae) are partial orders
+/-- Conditionally complete partial orders (with suprema and infima) are partial orders
 where every nonempty, directed set which is bounded above (respectively, below) has a
 least upper (respectively, greatest lower) bound. -/
 class ConditionallyCompletePartialOrder (α : Type*)