iInter_of_empty — Mathlib

English

If the index type is empty, the intersection over all indices is the universal set: ⋂ i, s i = univ.

Русский

Если множество индексов пусто, пересечение по всем индексам равно вселенамому множеству: ⋂ i, s i = univ.

LaTeX

$$$$ \\bigcap_{i} s(i) = \\operatorname{univ}. $$$$

Lean4

@[simp]
theorem iInter_of_empty [IsEmpty ι] (s : ι → Set α) : ⋂ i, s i = univ :=
  iInf_of_empty _

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