chainHeight — Mathlib

English

The chain height of a set s is the maximal length of a strictly ascending chain contained in s.

Русский

Высота цепи множества s — максимальная длина строго возрастающей цепи внутри s.

LaTeX

$$$ \\text{chainHeight}(s) = \\bigvee_{l \\in s.\\mathrm{subchain}} \\operatorname{length}(l) \\; (\\text{in } \\mathbb{N}^\\infty). $$$

Lean4

/-- The maximal length of a strictly ascending sequence in a partial order. -/
noncomputable def chainHeight : ℕ∞ :=
  ⨆ l ∈ s.subchain, length l

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