FGModuleCatEvaluation_apply — Mathlib

English

For f ∈ FGModuleCatDual K V and x ∈ V, the evaluation morphism satisfies ev(f ⊗ x) = f(x).

Русский

Для f ∈ FGModuleCatDual K V и x ∈ V, отображение-оценка удовлетворяет ev(f ⊗ x) = f(x).

LaTeX

$$(FGModuleCatEvaluation K V).hom (f ⊗ₜ x) = f.toFun x$$

Lean4

theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
    (FGModuleCatEvaluation K V).hom (f ⊗ₜ x) = f.toFun x :=
  contractLeft_apply f x

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