starConvex_iUnion — Mathlib

English

The union over i and j of star-convex sets s_i_j is star-convex at x if every s_i_j is star-convex at x.

Русский

Объединение по i и j множеств s_{i j} звездообразно относительно x, если каждое s_{i j} звездообразно относительно x.

LaTeX

$$$$\forall i,j,\ StarConvex_{\mathbb{K}}(x, s_{i j}) \Rightarrow StarConvex_{\mathbb{K}}(x, \bigcup_i \bigcup_j s_{i j}).$$$$

Lean4

theorem starConvex_iUnion {ι : Sort*} {s : ι → Set E} (hs : ∀ i, StarConvex 𝕜 x (s i)) : StarConvex 𝕜 x (⋃ i, s i) :=
  by
  rintro y hy a b ha hb hab
  rw [mem_iUnion] at hy ⊢
  obtain ⟨i, hy⟩ := hy
  exact ⟨i, hs i hy ha hb hab⟩

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