starConvex_sUnion — Mathlib

English

The union of a set of star-convex sets is star-convex.

Русский

Объединение множества звездообразных множеств также звездообразно.

LaTeX

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

Lean4

theorem starConvex_sUnion {S : Set (Set E)} (hS : ∀ s ∈ S, StarConvex 𝕜 x s) : StarConvex 𝕜 x (⋃₀ S) :=
  by
  rw [sUnion_eq_iUnion]
  exact starConvex_iUnion fun s => hS _ s.2

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