convex_halfSpace_im_lt

Mathlib.Analysis.Complex.Convex

URI: https://scilib.ai/kg/mathlib#convex_halfSpace_im_lt

English

For every real r, the half-space { c ∈ ℂ : Im(c) < r } is convex.

Русский

Для каждого вещественного r полуплоскость { c ∈ ℂ : Im(c) < r } выпукла.

LaTeX

$$$\\forall r\\in\\mathbb{R},\\; \\{ z\\in\\mathbb{C} : \\Im z < r \\} \\text{ выпукло в }\\mathbb{C}$$$

Lean4

theorem convex_halfSpace_im_lt : Convex ℝ {c : ℂ | c.im < r} :=
  convex_halfSpace_lt (.mk add_im smul_im) _

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

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

Разделы

Аффилиация

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