iInter — Mathlib

English

The intersection over an indexed family of closed-below sets is closed-below.

Русский

Пересечение по индексированному семейству множеств, замкнутых ниже, замкнуто ниже.

LaTeX

$$iInter {ι : Type u} {f : ι → Set Ordinal} {o : Ordinal} (h : ∀ i, IsClosedBelow (f i) o) : IsClosedBelow (Set.iInter fun i => f i) o$$

Lean4

theorem iInter {ι : Type u} {f : ι → Set Ordinal} {o : Ordinal} (h : ∀ i, IsClosedBelow (f i) o) :
    IsClosedBelow (⋂ i, f i) o :=
  IsClosedBelow.sInter fun _ ⟨i, hi⟩ ↦ hi ▸ (h i)

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