congr_arg

Mathlib.LinearAlgebra.Alternating.Basic

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

English

If x = y, then applying an alternating map yields equal outputs: f(x) = f(y).

Русский

Если x = y, то применение чередующего отображения даёт равные значения: f(x) = f(y).

LaTeX

$$$$x = y \\Rightarrow f(x) = f(y).$$$$

Lean4

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

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

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

Разделы

Аффилиация

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