Theorems · Theorem · general topology

edist_neg_neg

∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b : G), edist (-a) (-b) = edist a b

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddGroupPseudoEMetricSpaceIsIsometricVAddIsIsometricVAdd