add_smul_subset — Mathlib

English

For scalars a,b in α and a set s in a module, (a+b) • s is contained in a•s + b•s, expressing linearity of the action on sets.

Русский

Для скаляров a,b и множества s в модуле верно: (a+b) • s ⊆ a•s + b•s, т.е. линейность действия на множествах.

LaTeX

$$$ (a+b) \\cdot s \\subseteq a \\cdot s + b \\cdot s $$$

Lean4

theorem add_smul_subset (a b : α) (s : Set β) : (a + b) • s ⊆ a • s + b • s :=
  by
  rintro _ ⟨x, hx, rfl⟩
  simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)

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