English
The Colex order between s and t is equivalent to a subset relation between the corresponding set differences expressed via lowerClosure.
Русский
Порядок Коэкса между s и t эквивалентен отношению включения между соответствующими различиями множеств, выраженными через нижнюю замкну.
LaTeX
$$$$ s \\le t \\iff (\\operatorname{coe}(\\operatorname{ofColex} s) \\setminus \\operatorname{coe}(\\operatorname{ofColex} t)) \\subseteq \\operatorname{lowerClosure}(\\operatorname{coe}(\\operatorname{ofColex} t) \\setminus \\operatorname{coe}(\\operatorname{ofColex} s)) $$$$
Lean4
/-- The colexigraphic order is insensitive to removing the same elements from both sets. -/
theorem toColex_sdiff_lt_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) :
toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t :=
lt_iff_lt_of_le_iff_le' (toColex_sdiff_le_toColex_sdiff hut hus) <| toColex_sdiff_le_toColex_sdiff hus hut
