smul_nonempty_iff

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

If s and t are nonempty then s • t is nonempty.

Русский

Если s и t непусты, то s • t непусто.

LaTeX

$$$ s.Nonempty \rightarrow t.Nonempty \rightarrow (s \cdot t).Nonempty $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_nonempty_iff : (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  image₂_nonempty_iff

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

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

Разделы

Аффилиация

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