iUnion_empty

Mathlib.Data.Set.Lattice

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

English

The union over a family of empty sets is empty: ⋃_{ι} ∅ = ∅.

Русский

Объединение семейства пустых множеств равно пустому множеству: ⋃_{ι} ∅ = ∅.

LaTeX

$$$$\\bigcup_{i: \\iota} \\emptyset = \\emptyset$$$$

Lean4

@[simp]
theorem iUnion_empty : (⋃ _ : ι, ∅ : Set α) = ∅ :=
  iSup_bot

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

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

Разделы

Аффилиация

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