depth — Mathlib

English

The depth of a W-type tree is defined inductively by depth(⟨a,f⟩) = sup { depth(f(i)) : i ∈ β(a) } + 1.

Русский

Глубина дерева WType задаётся индуктивно: depth⟨a,f⟩ = sup{ depth(f(i)) : i ∈ β(a) } + 1.

LaTeX

$$$\text{depth}(\langle a,f\rangle) = \sup_{i\in \beta(a)} \text{depth}(f(i)) + 1.$$$

Lean4

/-- The depth of a finitely branching tree. -/
def depth : WType β → ℕ
  | ⟨_, f⟩ => (Finset.sup Finset.univ fun n => depth (f n)) + 1

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