apply_toDualLeft_symm_apply — Mathlib

English

For f in Dual R N and x in N, p(p.toDualLeft.symm f, x) = f(x).

Русский

Для f ∈ Dual R N и x ∈ N выполняется p(p.toDualLeft.symm f, x) = f(x).

LaTeX

$$$p\big(p.toDualLeft.symm\; f,\; x\big) = f(x)$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem apply_toDualLeft_symm_apply (f : Dual R N) (x : N) : p (p.toDualLeft.symm f) x = f x :=
  by
  have h := LinearEquiv.apply_symm_apply p.toDualLeft f
  rw [toDualLeft_apply] at h
  exact congrFun (congrArg DFunLike.coe h) x

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