convex_halfSpace_re_le — Mathlib

English

The closed half-space { c ∈ ℂ : Re(c) ≤ r } is convex for every real r.

Русский

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

LaTeX

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

Lean4

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

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