iInter_false

Mathlib.Data.Set.Lattice

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

English

If the index is the empty False-type, the intersection over a false-index family equals the universal set.

Русский

Если индекс пустой, пересечение над всеми элементами равно вселенной.

LaTeX

$$$ \bigcap_s {False} \to Set A = \mathsf{univ}$$$

Lean4

theorem iInter_false {s : False → Set α} : iInter s = univ :=
  iInf_false

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

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

Разделы

Аффилиация

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