Theorems · Theorem · general topology

IsometryEquiv.subRight_apply

∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c b : G),
  (IsometryEquiv.subRight c) b = b - c

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupPseudoEMetricSpaceIsIsometricVAdd