smul_nonempty

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

The product s • t is nonempty if and only if s and t are nonempty.

Русский

Произведение s • t непусто тогда и только тогда, когда s и t непусты.

LaTeX

$$$$ (s \cdot t) \neq \emptyset \iff s \neq \emptyset \land t \neq \emptyset $$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_nonempty : (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  image2_nonempty_iff

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

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

Разделы

Аффилиация

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