comap_mul_right_cobounded — Mathlib

English

If a ≠ 0, then right-multiplication by a preserves the cobounded filter: the comap of the cobounded filter along b ↦ b a equals the cobounded filter itself.

Русский

Если a ≠ 0, то умножение справа на a сохраняет фильтр cobounded: образующая фильтр совпадает с cobounded.

LaTeX

$$$\operatorname{comap}(\,\cdot a\,)(\operatorname{cobounded}\,\alpha) = \operatorname{cobounded}\,\alpha \quad (a \neq 0).$$$

Lean4

@[simp]
theorem comap_mul_right_cobounded {a : α} (ha : a ≠ 0) : comap (· * a) (cobounded α) = cobounded α :=
  Dilation.comap_cobounded (Dilation.mulRight a ha)

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