ofRealLI

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.ofRealLI

English

The canonical embedding of ℝ into ℂ is a real-linear isometry.

Русский

Каноническое вложение ℝ в ℂ — ℝ-линейная изометрия.

LaTeX

$$$ \\|\\ operatorname{ofRealLI}(x)\\| = |x| \\quad \\text{for all } x \\in \\mathbb{R}$$$

Lean4

/-- Linear isometry version of the canonical embedding of `ℝ` in `ℂ`. -/
def ofRealLI : ℝ →ₗᵢ[ℝ] ℂ :=
  ⟨ofRealAm.toLinearMap, norm_real⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru