sInter_empty

Mathlib.Data.Set.Lattice

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

English

The intersection over the empty collection is the universal set.

Русский

Пересечение пустой коллекции равно вселенному множество.

LaTeX

$$$ \bigcap_0 \emptyset = \text{univ} $$$

Lean4

@[simp]
theorem sInter_empty : ⋂₀ ∅ = (univ : Set α) :=
  sInf_empty

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

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

Разделы

Аффилиация

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