le_chainHeight_iff — Mathlib

English

For any n, ↑n ≤ s.chainHeight if and only if there exists l ∈ s.subchain with length l = n.

Русский

Для любого n, ↑n ≤ s.chainHeight тогда и только тогда, когда существует l ∈ s.subchain такое, что length(l) = n.

LaTeX

$$$ \\uparrow n \\le s.chainHeight \\iff \\exists l \\in s.\\mathrm{subchain}, \\operatorname{length}(l) = n. $$$

Lean4

theorem le_chainHeight_iff {n : ℕ} : ↑n ≤ s.chainHeight ↔ ∃ l ∈ s.subchain, length l = n :=
  (le_chainHeight_TFAE s n).out 0 1

Похожие утверждения