bilinearComp_zero_right — Mathlib

English

For p = (x,y) in E × Fℓ, the derivative-in-two-variables functional f.deriv₂(p) acts on q = (u,v) by f(x,v) + f(u,y).

Русский

Для p = (x,y) в E × Fℓ функционал f.deriv₂(p) действует на q = (u,v) как f(x,v) + f(u,y).

LaTeX

$$$(f.deriv\_2 p)(q) = f(p_1, q_2) + f(q_1, p_2)$, где $p=(p_1,p_2)$ и $q=(q_1,q_2)$$$

Lean4

@[simp]
theorem bilinearComp_zero_right {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gE : E' →SL[σ₁'] E} :
    bilinearComp f gE (0 : F' →SL[σ₂'] F) = 0 := by ext; simp

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