Theorems · Theorem · general topology

Metric.inductiveLimitDist_eq_dist

∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)},
  (∀ (n : ℕ), Isometry (f n)) →
    ∀ (x y : (n : ℕ) × X n) (m : ℕ) (hx : x.fst ≤ m) (hy : y.fst ≤ m),
      Metric.inductiveLimitDist f x y =
        dist (Nat.leRecOn hx (fun {k} => f k) x.snd) (Nat.leRecOn hy (fun {k} => f k) y.snd)

The predistance on the disjoint union Σ n, X n can be computed in any X k for large enough k.

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

2 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpace