English
If each s_i_j is star-convex at x, then the double indexed intersection is star-convex at x.
Русский
Если каждый s_{i j} звездообразно относительно x, то двойное индексированное пересечение звездообразно относительно x.
LaTeX
$$$$\forall i,j,\ StarConvex_{\mathbb{K}}(x, s_{i j}) \Rightarrow StarConvex_{\mathbb{K}}(x, \bigcap_i \bigcap_j s_{i j}).$$$$
Lean4
theorem starConvex_iInter₂ {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E} (h : ∀ i j, StarConvex 𝕜 x (s i j)) :
StarConvex 𝕜 x (⋂ (i) (j), s i j) :=
starConvex_iInter fun i => starConvex_iInter (h i)