isUpperSet_sInter — Mathlib

English

The intersection of a collection of upper sets is upper: if every s ∈ S is upper, then ⋂ S is upper.

Русский

Пересечение произвольной коллекции верхних множеств является верхним множеством: если каждое s ∈ S верхнее, то ⋂ S — верхнее.

LaTeX

$$$\forall S, (\forall s \in S, IsUpperSet s) \Rightarrow IsUpperSet(\bigcap S)$$$

Lean4

theorem isUpperSet_sInter {S : Set (Set α)} (hf : ∀ s ∈ S, IsUpperSet s) : IsUpperSet (⋂₀ S) := fun _ _ h =>
  forall₂_imp fun s hs => hf s hs h

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