smul_finset_nonempty

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.smul_finset_nonempty

English

(a • s).Nonempty ↔ s.Nonempty.

Русский

(a • s).непусто ↔ s не пусто.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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