biInter_empty

Mathlib.Data.Set.Lattice

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

English

If u is a family of sets indexed by α, then the intersection over the empty index set equals the universal set.

Русский

Пусть u : α → Set β. Тогда пересечение по пустому индексу равно все множество β.

LaTeX

$$$\\\\bigcap x \\\\in (\\\\empty : Set\\\\alpha), u(x) = \\\\mathrm{univ}$$$

Lean4

theorem biInter_empty (u : α → Set β) : ⋂ x ∈ (∅ : Set α), u x = univ :=
  iInf_emptyset

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

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

Разделы

Аффилиация

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