convex_halfSpace_im_gt

Mathlib.Analysis.Complex.Convex

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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