sInter_eq_univ — Mathlib

English

The intersection over S equals the universal set if and only if every member s ∈ S equals the universal set.

Русский

Пересечение над S равно вселенному множеству тогда и только тогда, когда каждый элемент S равен вселенному.

LaTeX

$$$ \bigcap S = \text{univ} \iff \forall s \in S, s = \text{univ} $$$

Lean4

@[simp]
theorem sInter_eq_univ {S : Set (Set α)} : ⋂₀ S = univ ↔ ∀ s ∈ S, s = univ :=
  sInf_eq_top

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