starConvex_iInter — Mathlib

English

If every s_i is star-convex at x, then the intersection over i of s_i is star-convex at x.

Русский

Если для каждого i множество s_i звездообразно относительно x, то пересечение всех s_i звездообразно относительно x.

LaTeX

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

Lean4

theorem starConvex_iInter {ι : Sort*} {s : ι → Set E} (h : ∀ i, StarConvex 𝕜 x (s i)) : StarConvex 𝕜 x (⋂ i, s i) :=
  sInter_range s ▸ starConvex_sInter <| forall_mem_range.2 h

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