map_mul_left_cobounded — Mathlib

English

For a nonzero a, left multiplication by a preserves coboundedness of filters (maps cobounded to cobounded).

Русский

Для ненулевого a левое умножение сохраняет свойство cobounded для фильтров.

LaTeX

$$$a \neq 0 \Rightarrow \mathrm{map}(a \cdot )(\mathrm{cobounded}(\alpha)) = \mathrm{cobounded}(\alpha).$$$

Lean4

@[simp]
theorem map_mul_left_cobounded {a : α} (ha : a ≠ 0) : map (a * ·) (cobounded α) = cobounded α :=
  DilationEquiv.map_cobounded (DilationEquiv.mulLeft a ha)

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