equivRealProdCLM — Mathlib

English

There exists a continuous linear isomorphism between ℂ and ℝ×ℝ given by z ↦ (Re z, Im z) and its inverse (a,b) ↦ a+bi.

Русский

Существует непрерывное линейное изоморфизм между ℂ и ℝ×ℝ, задаваемый z ↦ (Re z, Im z) и обратное (a,b) ↦ a+bi.

LaTeX

$$$$ \\mathbb{C} \\cong_{\\mathbb{R}} \\mathbb{R}^2, \\quad z \\mapsto (\\Re z, \\Im z), \\quad (a,b) \\mapsto a+bi. $$$$

Lean4

/-- The natural `ContinuousLinearEquiv` from `ℂ` to `ℝ × ℝ`. -/
@[simps! +simpRhs apply symm_apply_re symm_apply_im]
def equivRealProdCLM : ℂ ≃L[ℝ] ℝ × ℝ :=
  equivRealProdLm.toContinuousLinearEquivOfBounds 1 (√2) equivRealProd_apply_le' fun p =>
    norm_le_sqrt_two_mul_max (equivRealProd.symm p)

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