Mathlib Map

Theorems · Theorem · general topology

isometry_neg

∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G],
  Isometry Neg.neg
Defined in
Mathlib.Topology.MetricSpace.IsometricSMul
Cited by
2 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.

infEDist_neg_neg · cited by 2infEDist_neg_negquotient_norm_mk_eq · cited by 1quotient_norm_mk_eqAddGroup · cited by 4410AddGroupPseudoEMetricSpace · cited by 1536PseudoEMetricSpaceAddOpposite · cited by 452AddOppositeIsometry · cited by 230IsometryIsIsometricVAdd · cited by 74IsIsometricVAddedist_neg_neg · cited by 6edist_neg_negisometry_negCITED 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.