Mathlib Map

Theorems · Definition · general topology

Metric.inductivePremetric

{X : ℕ → Type u} →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    {f : (n : ℕ) → X n → X (n + 1)} → (∀ (n : ℕ), Isometry (f n)) → PseudoMetricSpace ((n : ℕ) × X n)

Premetric space structure on Σ n, X n.

Defined in
Mathlib.Topology.MetricSpace.Gluing
Cited by
1 results in Mathlib
Foundations
Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
MetricSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Metric.toInductiveLimit_commute · cited by 0Metric.toInductiveLimit_c…MetricSpace · cited by 1684MetricSpacePseudoMetricSpace · cited by 1550PseudoMetricSpaceENNReal.ofNNReal · cited by 1279ENNReal.ofNNRealIsometry · cited by 230IsometryNNReal.mk · cited by 94NNReal.mkMetric.inductiveLimitDist · cited by 1Metric.inductiveLimitDistUniformSpace.ofDist · cited by 1UniformSpace.ofDistBornology.ofDist · cited by 0Bornology.ofDistMetric.inductivePremetricCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.