isLowerSet_sInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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