disjSum_eq_empty

Mathlib.Data.Finset.Sum

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

English

The disjoint sum s.disjSum t is empty if and only if both s and t are empty.

Русский

Дизъюнктивная сумма s.disjSum t пуста тогда и только тогда, когда оба множества s и t пусты.

LaTeX

$$$ s.disjSum t = \emptyset \iff s = \emptyset \land t = \emptyset $$$

Lean4

@[simp]
theorem disjSum_eq_empty : s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅ := by simp [Finset.ext_iff]

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

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

Разделы

Аффилиация

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