continuousLinearMapOfBilin_apply — Mathlib

English

For v,w ∈ E, the inner product with the B♯-image equals B(v,w): ⟪B♯v, w⟫ = B v w.

Русский

Для любых v,w ∈ E имеет место ⟪B♯v, w⟫ = B(v,w).

LaTeX

$$\langle B^{\sharp} v, w \rangle = B(v)(w)$$

Lean4

@[simp]
theorem continuousLinearMapOfBilin_apply (v w : E) : ⟪B♯ v, w⟫ = B v w := by
  rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]

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