English
Re-states the same triad equivalences of chainHeight relations as a formalized TFAE assertion.
Русский
Повторно формулируются три эквивалентности для цепной высоты в виде утверждения TFAE.
LaTeX
$$TFAE [ s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l = length l', ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l ≤ length l' ]$$
Lean4
theorem chainHeight_eq_iSup_Ici : s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Ici i).chainHeight :=
by
apply le_antisymm
· refine iSup₂_le ?_
rintro (_ | ⟨x, xs⟩) h
· exact zero_le _
· apply le_trans _ (le_iSup₂ x (cons_mem_subchain_iff.mp h).1)
apply length_le_chainHeight_of_mem_subchain
refine ⟨h.1, fun i hi ↦ ⟨h.2 i hi, ?_⟩⟩
cases hi
· exact left_mem_Ici
rename_i hi
obtain - | h' := isChain_iff_pairwise.mp h.1
exact (h' _ hi).le
· exact iSup₂_le fun i _ ↦ chainHeight_mono Set.inter_subset_left
