coeff_inj — Mathlib

English

The map coeff: HVertexOperator Γ R V W → Γ → (V → W) is injective; i.e., if coeff A = coeff B as functions, then A = B.

Русский

Отображение coeff инъективно: если coeff(A) = coeff(B) то A = B.

LaTeX

$$$\mathrm{coeff} : HVertexOperator(\Gamma,R,V,W) \to \Gamma \to (V \to W)$ is injective.$$

Lean4

@[ext]
theorem coeff_inj : Function.Injective (coeff : HVertexOperator Γ R V W →ₗ[R] Γ → (V →ₗ[R] W)) :=
  by
  intro _ _ h
  ext v n
  exact congrFun (congrArg DFunLike.coe (congrFun h n)) v

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