Theorems · Theorem · general topology

Metric.preimage_add_right_eball

∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x + a) ⁻¹' Metric.eball b r = Metric.eball (b - a) r

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupPseudoEMetricSpaceIsIsometricVAdd