English
If z is a positive real number, then the slit plane is star-shaped with center z; i.e., every point of the slit plane can be connected to z by a line segment contained in the slit plane.
Русский
Если z — положительное вещественное число, то щелевая плоскость звездообразна относительно точки z; т.е. для любой точки w из щелевой плоскости отрезок от z до w лежит в щелевой плоскости.
LaTeX
$$$\\forall z\\in\\mathbb{C},\\ z>0:\\; \\mathrm{slitPlane}\\ \\text{ является звездообразной вокруг } z: \\forall w\\in \\mathrm{slitPlane},\\ \\forall t\\in[0,1],\\ (1-t)z + t w \\in \\mathrm{slitPlane}$$$
Lean4
/-- The slit plane is star-convex at a positive number. -/
theorem starConvex_slitPlane {z : ℂ} (hz : 0 < z) : StarConvex ℝ z slitPlane :=
Complex.compl_Iic_zero ▸ starConvex_compl_Iic hz
