English
Let s be a finite subset of α and a ∈ α. In the Colex order, s is less than the singleton {a} precisely when every element of s is strictly less than a.
Русский
Пусть s — конечное подмножество множества α, и a ∈ α. В порядке Ко-лекс s < {a} тогда и только тогда, когда каждый элемент s строго меньше a.
LaTeX
$$$$ \\operatorname{toColex}(s) < \\operatorname{toColex}({a}) \\iff \\forall b \\in s,\\ b < a $$$$
Lean4
/-- `s < {a}` in colex iff all elements of `s` are strictly less than `a`. -/
theorem toColex_lt_singleton : toColex s < toColex { a } ↔ ∀ b ∈ s, b < a :=
by
rw [lt_iff_le_and_ne, toColex_le_singleton, ne_eq, toColex_inj]
refine
⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_, fun h ↦
⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩ <;>
rintro rfl
· refine h.2 <| eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc ↦ (h.1 _ hc).2 hb⟩
· simp at h
