convex_halfSpace_re_lt — Mathlib

English

For every real r, the set { c ∈ ℂ : Re(c) < r } is convex in the real vector space structure of ℂ.

Русский

Для каждого действительного r множество { c ∈ ℂ : Re(c) < r } выпукло в вещественным векторном пространстве ℂ.

LaTeX

$$$\\forall r\\in\\mathbb{R},\\; \\{ z\\in\\mathbb{C} \\mid \\Re z < r \\} \\text{ выпукло в }\\mathbb{C} \\text{ как вещественный векторное пространство }$$

Lean4

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

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