Mathlib Map

Theorems · Theorem · general topology

Metric.Sigma.dist_same

∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (i : ι) (x y : E i),
  dist ⟨i, x⟩ ⟨i, y⟩ = dist x y
Defined in
Mathlib.Topology.MetricSpace.Gluing
Cited by
3 results in Mathlib
Foundations
Depth 92 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.Sigma.isometry_mk · cited by 1Sigma.isometry_mkMetric.Sigma.dist_triangle · cited by 0Sigma.dist_triangleMetric.Sigma.isOpen_iff · cited by 0Sigma.isOpen_iffReal · cited by 25697RealMetricSpace · cited by 1684MetricSpaceDist.dist · cited by 1539Dist.distSigma.dist_sameCITED BYCITES

Cites3

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

  • Realstatement · cited by 25,697
  • MetricSpacestatement and proof · cited by 1,684
  • Dist.diststatement and proof · cited by 1,539

Cited by3

Results whose statement or proof uses this declaration.