comap_cobounded_le — Mathlib

English

If f is Lipschitz with constant K between metric spaces α and β, then the pullback of the cobounded filter on β along f is contained in the cobounded filter on α.

Русский

Если f—липшицева функция между метрическими пространствами α и β с константой K, то прообразCobounded(β) вдоль f содержится в Cobounded(α).

LaTeX

$$$\\operatorname{comap}_{f}(\\operatorname{cobounded}(\\beta)) \\le \\operatorname{cobounded}(\\alpha)\\,.$$$

Lean4

theorem comap_cobounded_le (hf : LipschitzWith K f) : comap f (Bornology.cobounded β) ≤ Bornology.cobounded α :=
  (hf.toLocallyBoundedMap f).2

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