iInter_univ

Mathlib.Data.Set.Lattice

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

English

The intersection over all index positions of the universal set equals the universal set itself: ⋂_{ι} univ = univ.

Русский

Пересечение по всем индексам твёрдо равно всем множествам: ⋂_{ι} univ = univ.

LaTeX

$$$$\\bigcap_{i: \\iota} {\\text{univ}} = {\\text{univ}}$$$$

Lean4

@[simp]
theorem iInter_univ : (⋂ _ : ι, univ : Set α) = univ :=
  iInf_top

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

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

Разделы

Аффилиация

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