zero_smul_set_subset — Mathlib

English

Let α and β be types with a zero, and let α act on β via a SMulWithZero action. For any subset s of β, the image of s under the zero scalar (0 in α) consists only of the zero element of β; hence (0) • s ⊆ {0}.

Русский

Пусть α и β — типы с нулём, и α действует на β посредством нулевого скалярного действия. Для любого подмножества s ⊆ β образ s под действием нуля на α содержит только ноль β, т.е. (0) • s ⊆ {0}.

LaTeX

$$$ (0 : \alpha) \cdot s \subseteq \{0_\beta\} $$$

Lean4

theorem zero_smul_set_subset (s : Set β) : (0 : α) • s ⊆ 0 :=
  image_subset_iff.2 fun x _ ↦ zero_smul α x

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