English
The Colex order is defined by: s ≤ t iff for all a ∈ ofColex s, if a ∉ ofColex t then there exists b ∈ ofColex t with b ∉ ofColex s and a ≤ b.
Русский
Порядок Colex задан так: $s \le t$ тогда и только тогда, когда для любого $a$ из $ofColex(s)$, если $a \notin ofColex(t)$, то существует $b \in ofColex(t)$, такое что $b \notin ofColex(s)$ и $a \le b$.
LaTeX
$$$s \le t \iff \forall a, a \in ofColex(s) \to a \notin ofColex(t) \to \exists b \in ofColex(t),\; b \notin ofColex(s) \land a \le b$$$
Lean4
instance instPartialOrder : PartialOrder (Colex (Finset α))
where
le_refl _ _ ha ha' := (ha' ha).elim
le_antisymm _ _ hst hts := (antisymm_aux hst hts).antisymm (antisymm_aux hts hst)
le_trans s t u hst htu a has
hau := by
by_cases hat : a ∈ ofColex t
· have ⟨b, hbu, hbt, hab⟩ := htu hat hau
by_cases hbs : b ∈ ofColex s
· have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu hbs hbt
exact ⟨c, hcu, hcs, hab.trans hbc⟩
· exact ⟨b, hbu, hbs, hab⟩
· exact trans_aux hst htu has hat
