congr_fun

Mathlib.RingTheory.Bialgebra.Equiv

URI: https://scilib.ai/kg/mathlib#BialgEquiv.congr_fun

English

If e = e′ then e(x) = e′(x) for all x ∈ A.

Русский

Если e = e′, то для всякого x ∈ A выполняется e(x) = e′(x).

LaTeX

$$$e=e' \\Rightarrow e(x)=e'(x) \\text{ for all } x\\in A$$$

Lean4

protected theorem congr_fun (h : e = e') (x : A) : e x = e' x :=
  DFunLike.congr_fun h x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru