English
For a bilipschitz map f: α→β, a set s is bounded in the induced Bornology if and only if it is bounded in the original Bornology.
Русский
Для билилипшиц-функции f: α→β множество s ограничено в индуцированнойBornology тогда и только тогда, когда оно ограничено в исходнойBornology.
LaTeX
$$IsBounded_{induced f}(s) ⇔ Bornology.IsBounded(s)$$
Lean4
/-- If `f : α → β` is bilipschitz, then the pullback of the bornology on `β` through `f` agrees
with the bornology on `α`.
This can be used to provide the replacement equality when applying
`PseudoMetricSpace.replaceBornology`, 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 : Bornology α := inferInstanceAs (Bornology β)
```
Users should instead write something like:
```
instance : Bornology α := Bornology.induced (f : α → β)
```
in order to avoid abuse of the definitional equality `α := β`. -/
theorem isBounded_iff_of_bilipschitz (hf₁ : AntilipschitzWith K₁ f) (hf₂ : LipschitzWith K₂ f) (s : Set α) :
@IsBounded _ (induced f) s ↔ Bornology.IsBounded s :=
Filter.ext_iff.1 (bornology_eq_of_bilipschitz hf₁ hf₂) (sᶜ)
