congr

Mathlib.Data.FunLike.Basic

URI: https://scilib.ai/kg/mathlib#DFunLike.congr

English

If f = g and x = y, then f x = g y.

Русский

Если f = g и x = y, тогда f(x) = g(y).

LaTeX

$$$\forall f,g:\,F, \forall x,y:\,\alpha, (f = g) \Rightarrow (x = y) \Rightarrow f x = g y.$$$

Lean4

protected theorem congr {f g : F} {x y : α} (h₁ : f = g) (h₂ : x = y) : f x = g y :=
  congr (congr_arg _ h₁) h₂

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

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

Разделы

Аффилиация

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