wInner_zero_right

Mathlib.Analysis.RCLike.Inner

URI: https://scilib.ai/kg/mathlib#RCLike.wInner_zero_right

English

The real part of the extended functional at x equals fr(x) again (compatibility with real embedding).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem wInner_zero_right (w : ι → ℝ) (f : ∀ i, E i) : ⟪f, 0⟫_[𝕜, w] = 0 := by simp [wInner]

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

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

Разделы

Аффилиация

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