extendTo𝕜 — Mathlib

English

The real part of the extended functional at x equals fr(x).

Русский

Действительная часть значения расширенного функционала в x равна fr(x).

LaTeX

$$$ \\operatorname{Re}\\big( (fr.extendTo𝕜')(x) \\big) = fr(x) $$$

Lean4

/-- Extend `fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)` to `StrongDual 𝕜 F`. -/
noncomputable def extendTo𝕜 (fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) : StrongDual 𝕜 F :=
  fr.extendTo𝕜'

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