re_surjective — Mathlib

English

The real part map Re: ℂ → ℝ is surjective; for every r ∈ ℝ there exists z ∈ ℂ with Re(z) = r.

Русский

Действительная часть действует на ℂ и достигает любую заданную величину r ∈ ℝ; существует z ∈ ℂ с Re(z) = r.

LaTeX

$$$$\operatorname{re}: \mathbb{C} \to \mathbb{R} \text{ is surjective, i.e. } \forall r \in \mathbb{R},\ \exists z \in \mathbb{C},\ \operatorname{Re}(z) = r.$$$$

Lean4

theorem re_surjective : Surjective re := fun x => ⟨⟨x, 0⟩, rfl⟩

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