iInter_eq_univ — Mathlib

English

The finite intersection over a family of sets equals the universal set if and only if every member is universal: ⋂ i, s_i = univ ↔ ∀ i, s_i = univ.

Русский

Пересечение по всем множествам из семейства равно вселенному множеству тогда и только тогда, когда каждое множество из семейства равно вселенной: ⋂ i, s_i = univ ↔ ∀ i, s_i = univ.

LaTeX

$$$$\\bigcap_{i} s_i = \\text{univ} \\;\\iff\\; \\forall i, \\; s_i = \\text{univ}$$$$

Lean4

@[simp]
theorem iInter_eq_univ : ⋂ i, s i = univ ↔ ∀ i, s i = univ :=
  iInf_eq_top

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