doc: fix Codisjoint typo (#31066)

Author: vihdzp

Mathlib/Order/Disjoint.lean

@@ -200,7 +200,7 @@ variable [PartialOrder α] [OrderTop α] {a b c d : α}
 /-- Two elements of a lattice are codisjoint if their sup is the top element.
 
 Note that we define this without reference to `⊔`, as this allows us to talk about orders where
-the supremum is not unique, or where implement `Sup` would require additional `Decidable`
+the supremum is not unique, or where implementing `Sup` would require additional `Decidable`
 arguments. -/
 def Codisjoint (a b : α) : Prop :=
   ∀ ⦃x⦄, a ≤ x → b ≤ x → ⊤ ≤ x