starConvex_iInter₂ — Mathlib

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)

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