English
The chain height equals top element of ENat iff the chain is unbounded in height.
Русский
Высота цепи равна верхнему элементу ENat тогда и только тогда, когда высота цепи не ограничена.
LaTeX
$$$ s.chainHeight = \\top \\;\\iff\\; \\text{for all } n, \\exists l ∈ s.\\mathrm{subchain}, \\operatorname{length}(l) = n. $$$
Lean4
theorem chainHeight_eq_top_iff : s.chainHeight = ⊤ ↔ ∀ n, ∃ l ∈ s.subchain, length l = n :=
by
refine ⟨fun h n ↦ le_chainHeight_iff.1 (le_top.trans_eq h.symm), fun h ↦ ?_⟩
contrapose! h; obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 h
exact
⟨n + 1, fun l hs ↦
(Nat.lt_succ_iff.2 <| Nat.cast_le.1 <| (length_le_chainHeight_of_mem_subchain hs).trans_eq hn.symm).ne⟩
