mul_nonempty

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

The product s*t is nonempty iff both s and t are nonempty.

Русский

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

LaTeX

$$$(s * t).Nonempty \iff s.Nonempty \wedge t.Nonempty$$$

Lean4

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

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

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

Разделы

Аффилиация

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