inter — Mathlib

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⟩

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