English
Equivalently expressible: toColex s < toColex t iff there exists a witnessing a ∈ t \\ s with a ∉ s and ∀ b ∈ s, b ∉ t → b < a.
Русский
Эквивалентно: toColex s < toColex t эквивалентно существованию свидетеля a ∈ t\\s, которого нет в s, и для всех b ∈ s, b ∉ t → b < a.
LaTeX
$$$$ \\operatorname{toColex}(s) < \\operatorname{toColex}(t) \\iff \\exists a \\in t\\setminus s, a \\notin s \\land \\forall b \\in s, b \\notin t \\rightarrow b < a $$$$
Lean4
theorem toColex_le_toColex_iff_max'_mem :
toColex s ≤ toColex t ↔ ∀ hst : s ≠ t, (s ∆ t).max' (symmDiff_nonempty.2 hst) ∈ t :=
by
refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩
· set m := (s ∆ t).max' (symmDiff_nonempty.2 hst)
by_contra hmt
have hms : m ∈ s := by simpa [m, mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst
have ⟨b, hbt, hbs, hmb⟩ := h hms hmt
exact
lt_irrefl _ <|
(max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <| mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩
· have hst : s ≠ t := ne_of_mem_of_not_mem' has hat
refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩
simpa [mem_symmDiff, h hst] using max'_mem _ <| symmDiff_nonempty.2 hst
