English
A simp variant of the exists-forall characterization for the linear Colex order.
Русский
Упрощённая версия характеристики exists-forall для линейного порядка Коэкса.
LaTeX
$$$$ \\operatorname{lt\_simp} $$$$
Lean4
theorem lt_iff_exists_filter_lt : toColex s < toColex t ↔ ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a} :=
by
simp only [lt_iff_exists_forall_lt, mem_sdiff, filter_inj, and_assoc]
refine ⟨fun h ↦ ?_, ?_⟩
· let u := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
have mem_u {w : α} : w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w := by simp [u, and_assoc]
have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2
let m := max' _ hu
have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _
refine ⟨m, hmt, hms, fun a hma ↦ ⟨fun has ↦ not_imp_comm.1 (hm _ has) hma.asymm, fun hat ↦ ?_⟩⟩
by_contra has
have hau : a ∈ u := mem_u.2 ⟨hat, has, fun b hbs hbt ↦ (hm _ hbs hbt).trans hma⟩
exact hma.not_ge <| le_max' _ _ hau
· rintro ⟨w, hwt, hws, hw⟩
refine ⟨w, hwt, hws, fun a has hat ↦ ?_⟩
by_contra! hwa
exact hat <| (hw <| hwa.lt_of_ne <| ne_of_mem_of_not_mem hwt hat).1 has
