bornology_eq_of_bilipschitz — Mathlib

English

If f: α→β is bilipschitz, then the pullback of the cobounded bornology on β along f equals the cobounded bornology on α.

Русский

Если f: α→β билилипшиц, то обратная связь к coboundedBornology β по f равна coboundedBornology α.

LaTeX

$$$ cobounded_{(induced f)} = cobounded_α $$$

Lean4

/-- If `f : α → β` is bilipschitz, then the pullback of the bornology on `β` through `f` agrees
with the bornology on `α`. -/
theorem bornology_eq_of_bilipschitz (hf₁ : AntilipschitzWith K₁ f) (hf₂ : LipschitzWith K₂ f) :
    @cobounded _ (induced f) = cobounded α :=
  le_antisymm hf₂.comap_cobounded_le hf₁.tendsto_cobounded.le_comap

Похожие утверждения