congr_arg

Mathlib.Logic.Equiv.Defs

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

English

If f = g, then f x = g x for all x.

Русский

Если f = g, то для любого x верно f x = g x.

LaTeX

$$$\\forall {α} {β} {f g : Equiv α β}, f = g \\Rightarrow \\forall x, f x = g x.$$$

Lean4

protected theorem congr_arg {f : Equiv α β} {x x' : α} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

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

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

Разделы

Аффилиация

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