canLift — Mathlib

English

There is a canonical lifting of complex numbers to reals along the real-axis identification, reflecting Im(z) = 0.

Русский

Существует каноническое восхождение комплексных чисел к вещественным вдоль идентификации по действительной оси, отражающее Im(z) = 0.

LaTeX

$$$\\{ z \in \\mathbb{C} \mid \\operatorname{Im}(z) = 0 \\} \\cong \\mathbb{R}.$$$

Lean4

instance canLift : CanLift ℂ ℝ (↑) fun z => z.im = 0 where prf z hz := ⟨z.re, ext rfl hz.symm⟩

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