convex_closed_sInter — Mathlib

English

If S is a collection of subsets of E such that every member s in S is convex and closed, then the intersection ⋂₀ S is convex and closed.

Русский

Если S — множество подмножеств пространства E, и каждое s ∈ S выпукло и замкнуто, то ⋂₀ S выпукло и замкнуто.

LaTeX

$$$\forall S\,\forall h\,(\forall s\in S,\ Convex 𝕜 s \wedge IsClosed s) \Rightarrow Convex 𝕜 (\bigcap_{s\in S} s) \wedge IsClosed (\bigcap_{s\in S} s)$$$

Lean4

theorem convex_closed_sInter {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s) :
    Convex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S) :=
  ⟨fun _ hx => starConvex_sInter fun _ hs => (h _ hs).1 <| hx _ hs, isClosed_sInter fun _ hs => (h _ hs).2⟩

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