English
Let S be a nonempty collection of sets. If every member s in S is RelLowerSet with respect to P, then the intersection of all members of S is RelLowerSet with respect to P.
Русский
Пусть S — непустое множество множеств. Если каждый элемент s ∈ S является RelLowerSet относительно P, то ⋂₀ S является RelLowerSet относительно P.
LaTeX
$$$S \neq \varnothing \;\to\; (\forall s \in S, IsRelLowerSet s P) \Rightarrow IsRelLowerSet (\bigcap_{s \in S} s) P$$$
Lean4
protected theorem sInter {S : Set (Set α)} (hS : S.Nonempty) (hf : ∀ s ∈ S, IsRelLowerSet s P) :
IsRelLowerSet (⋂₀ S) P := fun b mb ↦ by
obtain ⟨s₀, ms₀⟩ := hS
refine ⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩
