sInter — Mathlib

English

If each C in a family S is closed below o, then their intersection is closed below o.

Русский

Если каждый элемент C множества S замкнут ниже o, то их пересечение замкнуто ниже o.

LaTeX

$$IsClosedBelow.sInter (h : ∀ C ∈ S, IsClosedBelow C o) : IsClosedBelow (⋂₀ S) o$$

Lean4

theorem sInter {o : Ordinal} {S : Set (Set Ordinal)} (h : ∀ C ∈ S, IsClosedBelow C o) : IsClosedBelow (⋂₀ S) o :=
  by
  rw [isClosedBelow_iff]
  intro p plto pAcc C CmemS
  exact (h C CmemS).forall_lt p plto (pAcc.mono (sInter_subset_of_mem CmemS))

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