English
The intersection of two star-convex sets with the same center is star-convex.
Русский
Пересечение двух звездообразных множеств относительно одной точки является звездообразным.
LaTeX
$$$$StarConvex_{\mathbb{K}}(x,s) \land StarConvex_{\mathbb{K}}(x,t) \Rightarrow StarConvex_{\mathbb{K}}(x, s \cap t).$$$$
Lean4
theorem inter (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∩ t) := fun _ hy _ _ ha hb hab =>
⟨hs hy.left ha hb hab, ht hy.right ha hb hab⟩