Theorems · Theorem · general topology

Congruent.comp_left_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 (f ∘ v₁) v₂ ↔ Congruent v₁ v₂)

Defined in: Mathlib.Topology.MetricSpace.Congruence
Cited by: 1 results in Mathlib
Foundations: Depth 150 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.

Cites7

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 · cited by 37
Congruent.transproof · cited by 3
Congruent.comp_leftproof · cited by 1
Congruent.reflproof · cited by 1
Congruent.comp_rightproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

Congruent.comp_right_iffproof · cited by 0