convex_halfSpace_im_ge

Mathlib.Analysis.Complex.Convex

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

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 \\le \\Im z \\} \\text{ выпукло в }\\mathbb{C}$$$

Lean4

theorem convex_halfSpace_im_ge : Convex ℝ {c : ℂ | r ≤ c.im} :=
  convex_halfSpace_ge (.mk add_im smul_im) _

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

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

Разделы

Аффилиация

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