Mathlib Map

Theorems · Theorem · general topology

edist_sub_left

∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b c : G), edist (a - b) (a - c) = edist b c
Defined in
Mathlib.Topology.MetricSpace.IsometricSMul
Cited by
0 results in Mathlib
Foundations
Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddGroupPseudoEMetricSpaceIsIsometricVAddIsIsometricVAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsometryEquiv.subLeft · cited by 4IsometryEquiv.subLeftENNReal · cited by 9879ENNRealAddGroup · cited by 4410AddGroupPseudoEMetricSpace · cited by 1536PseudoEMetricSpacesub_eq_add_neg · cited by 1023sub_eq_add_negEDist.edist · cited by 735EDist.edistAddOpposite · cited by 452AddOppositeIsIsometricVAdd · cited by 74IsIsometricVAddedist_neg_neg · cited by 6edist_neg_negedist_add_left · cited by 2edist_add_leftedist_sub_leftCITED BYCITES

Cites9

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

Cited by1

Results whose statement or proof uses this declaration.