union — Mathlib

English

The union of any family of star-convex sets with the same center is star-convex.

Русский

Объединение любой семейства звездообразных множеств относительно одной точки остаётся звездообразным.

LaTeX

$$$$\big(\forall i, StarConvex_{\mathbb{K}}(x, s_i)\big) \Rightarrow StarConvex_{\mathbb{K}}(x, \bigcup_i s_i).$$$$

Lean4

theorem union (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∪ t) :=
  by
  rintro y (hy | hy) a b ha hb hab
  · exact Or.inl (hs hy ha hb hab)
  · exact Or.inr (ht hy ha hb hab)

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