extendTo𝕜'_apply — Mathlib

English

The value of the extended functional at x is fr(x) − i fr(i x) (definition).

Русский

Значение расширенного функционала в точке x задается как fr(x) − i fr(i x) (определение).

LaTeX

$$$ (fr.extendTo𝕜')(x) = (fr(x) : 𝕜) - i (fr(i x) : 𝕜) $$$

Lean4

theorem extendTo𝕜'_apply (fr : StrongDual ℝ F) (x : F) :
    fr.extendTo𝕜' x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) :=
  rfl

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