smul_set_nonempty

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.smul_set_nonempty

English

(a · s) Nonempty iff s Nonempty

Русский

(a · s) Не пустое тогда и только тогда, когда s не пусто

LaTeX

$$$ (a \\cdot s) \\neq \\varnothing \\iff s \\neq \\varnothing $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_set_nonempty : (a • s).Nonempty ↔ s.Nonempty :=
  image_nonempty

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

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

Разделы

Аффилиация

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