smul_set_univ₀ — Mathlib

English

For a ≠ 0, a • univβ = univβ; i.e., the whole universe is preserved under nonzero smul.

Русский

Для a ≠ 0, a • универсума β = универсума β; то есть вся вселенная сохраняется под ненулевым умножением.

LaTeX

$$$ (ha : a \neq 0) (univ : Set \beta), a \cdot (\mathrm{univ}) = \mathrm{univ} $$$

Lean4

theorem smul_set_univ₀ (ha : a ≠ 0) : a • (univ : Set β) = univ :=
  image_univ_of_surjective <| MulAction.surjective₀ ha

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