congr_fun

Mathlib.LinearAlgebra.Alternating.Basic

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

English

If two alternating maps are equal, then their values agree on every input.

Русский

Если два чередующихся отображения равны, то они совпадают на всех входах.

LaTeX

$$$$f = g \\Rightarrow \\forall x, f(x) = g(x).$$$$

Lean4

protected theorem congr_fun {f g : M [⋀^ι]→ₗ[R] N} (h : f = g) (x : ι → M) : f x = g x :=
  congr_arg (fun h : M [⋀^ι]→ₗ[R] N => h x) h

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

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

Разделы

Аффилиация

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