Theorems · Theorem · general topology

Isometry.coveringNumber_image

∀ {Y : Type u_2} [inst : PseudoEMetricSpace Y] {ε : NNReal} {X : Type u_3} [inst_1 : EMetricSpace X] {f : X → Y},
  Isometry f → ∀ {A : Set X}, Metric.coveringNumber ε (f '' A) = Metric.coveringNumber ε A

The covering number of the image of a set under an injective isometry is equal to the covering number of the set. See Isometry.coveringNumber_image' for the version in a PseudoEMetricSpace and not an EMetricSpace, for which an additional injectivity assumption is needed.

Defined in

Mathlib.Topology.MetricSpace.CoveringNumbers

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceEMetricSpace