English
Let S be a nonempty collection of sets. If every member s in S is RelUpperSet with respect to P, then the intersection of all members of S is RelUpperSet with respect to P.
Русский
Пусть S — непустое множество множеств. Если каждый элемент s ∈ S является RelUpperSet относительно P, то ⋂₀ S является RelUpperSet относительно P.
LaTeX
$$$S \neq \varnothing \;\to\; (\forall s \in S, IsRelUpperSet s P) \Rightarrow IsRelUpperSet (\bigcap_{s \in S} s) P$$$
Lean4
protected theorem sInter {S : Set (Set α)} (hS : S.Nonempty) (hf : ∀ s ∈ S, IsRelUpperSet s P) :
IsRelUpperSet (⋂₀ 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⟩
