extendTo𝕜'_apply

Mathlib.Analysis.RCLike.Extend

URI: https://scilib.ai/kg/mathlib#LinearMap.extendTo𝕜'_apply

English

For any fr, x, the value of the extended functional is fr(x) − i fr(i x).

Русский

Для любого fr и элемента x значение расширенного функционала равно fr(x) − i fr(i x).

LaTeX

$$$ (fr)^{\\!\\prime}(x) = (fr(x) : 𝕜) - i \\,(fr(i x) : 𝕜) $$$

Lean4

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

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

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

Разделы

Аффилиация

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