union_empty_iff

Mathlib.Data.Set.Basic

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

English

For any sets S and T, S ∪ T = ∅ if and only if S = ∅ and T = ∅.

Русский

Для любых множеств S и T верно: S ∪ T = ∅ тогда и только тогда, когда S = ∅ и T = ∅.

LaTeX

$$$S \cup T = \emptyset \iff S = \emptyset \land T = \emptyset$$$

Lean4

@[simp]
theorem union_empty_iff {s t : Set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ :=
  by
  simp only [← subset_empty_iff]
  exact union_subset_iff

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

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

Разделы

Аффилиация

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