starConvex_sInter — Mathlib

English

The intersection over an index set S of star-convex sets is star-convex.

Русский

Пересечение множества множеств, каждое звездообразно относительно x, также звездообразно относительно x.

LaTeX

$$$$\Big(\forall s\in S,\ StarConvex_{\mathbb{K}}(x,s)\Big) \Rightarrow StarConvex_{\mathbb{K}}(x, \bigcap S).$$$$

Lean4

theorem starConvex_sInter {S : Set (Set E)} (h : ∀ s ∈ S, StarConvex 𝕜 x s) : StarConvex 𝕜 x (⋂₀ S) :=
  fun _ hy _ _ ha hb hab s hs => h s hs (hy s hs) ha hb hab

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