Theorems · Theorem · general topology

EMetric.preimage_mul_right_closedBall

Deprecated since 2026-01-24Use Metric.preimage_mul_right_closedEBall instead.

∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x * a) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (b / a) r

Alias of Metric.preimage_mul_right_closedEBall.

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupPseudoEMetricSpaceIsIsometricSMul