congr_fun

Mathlib.Algebra.Algebra.Equiv

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

English

Extensionality principle for AlgEquiv: equality determined by action on inputs.

Русский

Принцип экстенсивности для AlgEquiv: равенство определяется действием на входах.

LaTeX

$$$\\forall f,g, (\\forall a, f(a)=g(a)) \\Rightarrow f=g$$$

Lean4

protected theorem congr_fun {f g : A₁ ≃ₐ[R] A₂} (h : f = g) (x : A₁) : f x = g x :=
  DFunLike.congr_fun h x

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

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

Разделы

Аффилиация

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