comap_cobounded — Mathlib

English

For every dilation-like map f, the comap of cobounded β under f equals cobounded α; i.e., the preimage of cobounded β through f is exactly cobounded α.

Русский

Для любого отображения, подобного дилатации, образ-обратное взятие cobounded β через f равно cobounded α; то есть предобраз cobounded β при f совпадает с cobounded α.

LaTeX

$$$\operatorname{comap} f (\operatorname{cobounded} \beta) = \operatorname{cobounded} \alpha$$$

Lean4

@[simp]
theorem comap_cobounded : Filter.comap f (cobounded β) = cobounded α :=
  le_antisymm (lipschitz f).comap_cobounded_le (tendsto_cobounded f).le_comap

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