congr_fun

Mathlib.RingTheory.Coalgebra.Equiv

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

English

If two coalgebra equivalences are equal, then their actions on any input are equal pointwise.

Русский

Если две коалгебраические эквивалентности равны, то их действия на любой вход равны по точкам.

LaTeX

$$$e = e' \\Rightarrow \\forall x, e(x) = e'(x)$$$

Lean4

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

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

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

Разделы

Аффилиация

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