reCLM — Mathlib

English

There is a continuous linear map from ℂ to ℝ that sends z to Re z.

Русский

Существует непрерывное линейное отображение ℂ → ℝ, отправляющее z в Re z.

LaTeX

$$$$ \\mathrm{reCLM} : \\mathbb{C} \\to_{\\mathbb{R}} \\mathbb{R}, \\quad z \\mapsto \\Re z. $$$$

Lean4

/-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
def reCLM : ℂ →L[ℝ] ℝ :=
  reLm.mkContinuous 1 fun x => by simp [abs_re_le_norm]

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