Theorems · Theorem · general topology

congruent_iff_pairwise_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₂ ↔ Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Congruence holds if and only if all extended distances between points with different indices are the same.

Defined in

Mathlib.Topology.MetricSpace.Congruence

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace