coeFn_injective

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

If two affine maps are equal, they take the same value at any input.

Русский

Если две аффинные отображения равны, то они принимают одинаковые значения на любом входе.

LaTeX

$$f = g -> f x = g x$$

Lean4

theorem coeFn_injective : @Function.Injective (P1 →ᵃ[k] P2) (P1 → P2) (⇑) :=
  DFunLike.coe_injective

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

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

Разделы

Аффилиация

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