English
For any positive real x, the slit plane is star-shaped with center the real point x on the real axis; i.e., the segment from x to any point of the slit plane lies in the slit plane.
Русский
При любом положительном действительном x щелевая плоскость звездообразна относительно точки x на вещественной оси; отрезок от x до любой точки щелевой плоскости принадлежит ей.
LaTeX
$$$\\forall x\\in\\mathbb{R},\\ x>0:\\; \\mathrm{slitPlane} \\text{ звездообразна относительно } x: \\forall w\\in \\mathrm{slitPlane},\\ \\forall t\\in[0,1],\\ (1-t)x + t w \\in \\mathrm{slitPlane}$$$
Lean4
/-- The slit plane is star-shaped at a positive real number. -/
theorem starConvex_ofReal_slitPlane {x : ℝ} (hx : 0 < x) : StarConvex ℝ (↑x) slitPlane :=
starConvex_slitPlane <| zero_lt_real.2 hx
