ofRealCLM — Mathlib

English

The real-to-complex canonical embedding as a continuous linear map: ofRealCLM : ℝ →L[ℝ] ℂ.

Русский

Каноническое линейно-изометрическое вложение ℝ в ℂ в виде непрерывного линейного отображения.

LaTeX

$$$ ofRealCLM : \\mathbb{R} \\rightarrow_{\\mathbb{R}}^{\\mathbb{C}} \\mathbb{C} \\quad( x \\mapsto x )$$$

Lean4

/-- Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`. -/
def ofRealCLM : ℝ →L[ℝ] ℂ :=
  ofRealLI.toContinuousLinearMap

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