English
The chainHeight comparison between s and t is equivalent to the typical three-way equivalence (TFAE) involving length-equality and length-inequality conditions on subchains.
Русский
Сравнение цепной высоты между s и t эквивалентно тройному утверждению о равенстве/неравенстве длин подцепочек.
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_le_chainHeight_TFAE (s : Set α) (t : Set β) :
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'] :=
by
tfae_have 1 ↔ 3 := by convert ← chainHeight_add_le_chainHeight_add s t 0 0 <;> apply add_zero
tfae_have 2 ↔ 3 := by
refine forall₂_congr fun l _ ↦ ?_
simp_rw [← (le_chainHeight_TFAE t l.length).out 1 2, eq_comm]
tfae_finish
