starConvex_singleton — Mathlib

English

If every s_i is star-convex at x, then the indexed intersection ⋂_i s_i is star-convex at x.

Русский

Если каждый s_i звездообразен относительно x, то проиндексированное пересечение ⋂_i s_i звездообразно относительно x.

LaTeX

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

Lean4

theorem starConvex_singleton (x : E) : StarConvex 𝕜 x { x } :=
  by
  rintro y (rfl : y = x) a b _ _ hab
  exact Convex.combo_self hab _

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