convex_halfSpace_re_ge — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem convex_halfSpace_re_ge : Convex ℝ {c : ℂ | r ≤ c.re} :=
  convex_halfSpace_ge (.mk add_re smul_re) _

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