comap_mul_left_cobounded — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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