Mathlib Map

Theorems · Theorem · general topology

edist_mul_right

∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  edist (a * c) (b * c) = edist a b
Defined in
Mathlib.Topology.MetricSpace.IsometricSMul
Cited by
2 results in Mathlib
Foundations
Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
MulPseudoEMetricSpaceIsIsometricSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

edist_inv_inv · cited by 6edist_inv_invedist_div_right · cited by 0edist_div_rightENNReal · cited by 9879ENNRealPseudoEMetricSpace · cited by 1536PseudoEMetricSpaceMulOpposite · cited by 1135MulOppositeEDist.edist · cited by 735EDist.edistIsIsometricSMul · cited by 74IsIsometricSMulisometry_mul_right · cited by 2isometry_mul_rightedist_mul_rightCITED BYCITES

Cites6

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.