English
The following are equivalent: (i) n ≤ s.chainHeight; (ii) there exists l ∈ s.subchain with length l = n; (iii) there exists l ∈ s.subchain with n ≤ length l.
Русский
Следующие высказывания эквивалентны: (i) n ≤ s.chainHeight; (ii) существует l ∈ s.subchain, такое что length(l) = n; (iii) существует l ∈ s.subchain, такое что n ≤ length(l).
LaTeX
$$$ \\text{TFAE}\\,[\\, n ≤ s.chainHeight, \\exists l \\in s.\\mathrm{subchain}, \\operatorname{length}(l) = n, \\exists l \\in s.\\mathrm{subchain}, n ≤ \\operatorname{length}(l) \]$$$
Lean4
theorem le_chainHeight_TFAE (n : ℕ) :
TFAE [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, length l = n, ∃ l ∈ s.subchain, n ≤ length l] :=
by
tfae_have 1 → 2 := s.exists_chain_of_le_chainHeight
tfae_have 2 → 3 := fun ⟨l, hls, he⟩ ↦ ⟨l, hls, he.ge⟩
tfae_have 3 → 1 := fun ⟨l, hs, hn⟩ ↦ le_iSup₂_of_le l hs (WithTop.coe_le_coe.2 hn)
tfae_finish
