wInner_neg_right

Mathlib.Analysis.RCLike.Inner

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

English

The second argument negation yields negation of inner product: ⟪f, -g⟫ = −⟪f, g⟫.

Русский

Отрицание второго аргумента даёт отрицание скалярного произведения.

LaTeX

$$$ \\langle f, -g \\rangle_{𝕜,[w]} = -\\langle f, g \\rangle_{𝕜,[w]} $$$

Lean4

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

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

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

Разделы

Аффилиация

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