smul_zero

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.smul_zero

English

Generalized version with either c ≠ 0 or I = univ: c • I.pi s = I.pi (c • s).

Русский

Обобщенная версия: либо c ≠ 0, либо I = univ: c • I.pi s = I.pi (c • s).

LaTeX

$$$h \lor I = \mathrm{univ} \implies h.something \implies c \cdot I.\pi s = I.\pi (c \cdot s)$$$

Lean4

theorem smul_zero (hs : s.Nonempty) : s • (0 : Set β) = 0 :=
  s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru