English
If f: α→β is bilipschitz with constants K1 and K2, then the pullback of the uniformity on β along f equals the uniformity on α.
Русский
Если f: α→β билилипшиц с константами K1, K2, то проекция униформности β по f равна униформности α.
LaTeX
$$$\\mathcal{U}_α = (\\mathrm{comap}_f)\\,\\mathcal{U}_β$ under bilipschitz, i.e. 𝓤[(inferInstance).comap f] = 𝓤 α$$
Lean4
/-- 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 `α := β`. -/
theorem uniformity_eq_of_bilipschitz (hf₁ : AntilipschitzWith K₁ f) (hf₂ : LipschitzWith K₂ f) :
𝓤[(inferInstance : UniformSpace β).comap f] = 𝓤 α :=
hf₁.isUniformInducing hf₂.uniformContinuous |>.comap_uniformity
