congr_arg

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The function-like structure of affine maps is injective with respect to coercion.

Русский

Структура типа affine map как функции инъективна по отношению к приведениям.

LaTeX

$$Injectivity of coe$$

Lean4

protected theorem congr_arg (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) : f x = f y :=
  congr_arg _ h

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

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

Разделы

Аффилиация

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