imCLM — Mathlib

English

The imaginary-part in a continuous linear map setting, imCLM, is a continuous linear map from K to Real.

Русский

Мнимая часть в рамках непрерывного линейного отображения — imCLM — непрерывное линейное отображение от K в Real.

LaTeX

$$$\text{imCLM}: K \to^{{\text{StrongDual}}} \mathbb{R}$$$

Lean4

/-- The imaginary part in an `RCLike` field, as a continuous linear map. -/
noncomputable def imCLM : StrongDual ℝ K :=
  imLm.mkContinuous 1 fun x => by
    rw [one_mul]
    exact abs_im_le_norm x

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