toDual_symm_apply

Mathlib.Analysis.InnerProductSpace.Dual

URI: https://scilib.ai/kg/mathlib#InnerProductSpace.toDual_symm_apply

← MathLib Explorer

English

The adjoint relationship holds: the inner product of the preimage of y with x equals y acting on x.

Русский

Соотношение сопряжённости: ∑⟪(toDual 𝕜 E).symm y, x⟫ = y(x).

LaTeX

$$\langle (toDual 𝕜 E).symm y, x \rangle = y(x)$$

Lean4

@[simp]
theorem toDual_symm_apply {x : E} {y : StrongDual 𝕜 E} : ⟪(toDual 𝕜 E).symm y, x⟫ = y x :=
  by
  rw [← toDual_apply]
  simp only [LinearIsometryEquiv.apply_symm_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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