convex_halfSpace_re_gt

Mathlib.Analysis.Complex.Convex

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

English

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

Русский

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

LaTeX

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

Lean4

theorem convex_halfSpace_re_gt : Convex ℝ {c : ℂ | r < c.re} :=
  convex_halfSpace_gt (.mk add_re smul_re) _

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

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

Разделы

Аффилиация

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