congr_arg

Mathlib.RingTheory.Coalgebra.Equiv

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

English

If two coalgebra equivalences are equal, then applying them to any element yields equal results.

Русский

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

LaTeX

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

Lean4

protected theorem congr_arg {x x'} : x = x' → e x = e x' :=
  DFunLike.congr_arg e

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

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

Разделы

Аффилиация

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