Theorems · Theorem · general topology

Congruent.comp_right_iff

∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₂ → P₃},
  Isometry f → (Congruent v₁ (f ∘ v₂) ↔ Congruent v₁ v₂)

Defined in: Mathlib.Topology.MetricSpace.Congruence
Cited by: 0 results in Mathlib
Foundations: Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace PseudoEMetricSpace PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

PseudoEMetricSpacestatement and proof · cited by 1,536
Isometrystatement and proof · cited by 230
Congruentstatement and proof · cited by 37
congruent_commproof · cited by 1
Congruent.comp_left_iffproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.