Mathlib Map

Theorems · Theorem · general topology

Congruent.edist_eq

∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

A congruence preserves extended distance. Forward direction of congruent_iff_edist_eq.

Defined in
Mathlib.Topology.MetricSpace.Congruence
Cited by
2 results in Mathlib
Foundations
Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PseudoEMetricSpacePseudoEMetricSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Congruent.index_map · cited by 1Congruent.index_mapCongruent.index_equiv · cited by 0Congruent.index_equivENNReal · cited by 9879ENNRealPseudoEMetricSpace · cited by 1536PseudoEMetricSpaceEDist.edist · cited by 735EDist.edistCongruent · cited by 37Congruentcongruent_iff_edist_eq · cited by 2congruent_iff_edist_eqCongruent.edist_eqCITED BYCITES

Cites5

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

Cited by2

Results whose statement or proof uses this declaration.