inductiveLimitDist — Mathlib

English

The predistance on the disjoint union Σ n X_n is given by inductiveLimitDist.

Русский

Предочередное расстояние на дизъюнктивном объединении Σ_n X_n задаётся функцией inductiveLimitDist.

LaTeX

$$$\mathrm{inductiveLimitDist} : (\forall n, X_n \to X_{n+1}) \to (\Sigma n, X_n) \times (\Sigma n, X_n) \to \mathbb{R}$$$

Lean4

/-- Predistance on the disjoint union `Σ n, X n`. -/
def inductiveLimitDist (f : ∀ n, X n → X (n + 1)) (x y : Σ n, X n) : ℝ :=
  dist (leRecOn (le_max_left x.1 y.1) (f _) x.2 : X (max x.1 y.1))
    (leRecOn (le_max_right x.1 y.1) (f _) y.2 : X (max x.1 y.1))

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