congr_fun — Mathlib

English

If two LieDerivations are equal, then they produce equal values on each element of L; i.e., equality transfers pointwise under evaluation.

Русский

Если два LieDerivation равны, то их значения на каждом элементе L равны; тождество переходит точечно при применении к элементу.

LaTeX

$$$D_1 = D_2 \;\Rightarrow\; \forall a\in L,\; D_1(a)=D_2(a)$$$

Lean4

theorem congr_fun (h : D1 = D2) (a : L) : D1 a = D2 a :=
  DFunLike.congr_fun h a

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