Theorems · Theorem · general topology

uniformity_eq_of_bilipschitz

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K₁ K₂ : NNReal}
  {f : α → β}, AntilipschitzWith K₁ f → LipschitzWith K₂ f → uniformity α = uniformity α

If f : α → β is bilipschitz, then the pullback of the uniformity on β through f agrees with the uniformity on α. This can be used to provide the replacement equality when applying PseudoMetricSpace.replaceUniformity, which can be useful when following the forgetful inheritance pattern when creating type synonyms. Important Note: if α is some synonym of a type β (at default transparency), and f : α ≃ β is some bilipschitz equivalence, then instead of writing: `` instance : UniformSpace α := inferInstanceAs (UniformSpace β) ` Users should instead write something like: ` instance : UniformSpace α := (inferInstance : UniformSpace β).comap f ` in order to avoid abuse of the definitional equality α := β`.

Defined in

Mathlib.Topology.MetricSpace.Bilipschitz

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace