starConvex_iUnion₂ — Mathlib

English

The (arbitrary) intersection of star-convex sets with the same center is star-convex.

Русский

Пересечение произвольного числа звездообразных множеств относительно x звездообразно.

LaTeX

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

Lean4

theorem starConvex_iUnion₂ {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E} (h : ∀ i j, StarConvex 𝕜 x (s i j)) :
    StarConvex 𝕜 x (⋃ (i) (j), s i j) :=
  starConvex_iUnion fun i => starConvex_iUnion (h i)

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