congr_fun — Mathlib

English

Let f and g be two equivariant additive monoid homomorphisms from A to B. If f equals g, then for every element x in A, we have f(x) = g(x).

Русский

Пусть f и g — эквариантные адитивные моноид-гомоморфизмы из A в B. Если f = g, то для каждого элемента x из A выполняается f(x) = g(x).

LaTeX

$$$ (f=g) \\Rightarrow \\forall x:A,\\; f(x)=g(x) $$$

Lean4

protected theorem congr_fun {f g : A →ₑ+[φ] B} (h : f = g) (x : A) : f x = g x :=
  DFunLike.congr_fun h _

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