starConvex_one_slitPlane

Mathlib.Analysis.Complex.Convex

URI: https://scilib.ai/kg/mathlib#Complex.starConvex_one_slitPlane

English

The slit plane is star-shaped with center 1 on the real axis.

Русский

Щелевая плоскость звездообразна относительно точки 1 на вещественной оси.

LaTeX

$$$\\operatorname{StarConvex}_{\\mathbb{R}}(1, \\mathrm{slitPlane})$$$

Lean4

/-- The slit plane is star-shaped at `1`. -/
theorem starConvex_one_slitPlane : StarConvex ℝ 1 slitPlane :=
  starConvex_slitPlane one_pos

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru