coeFn_injective

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

The map from affine equivalences to their underlying functions is injective.

Русский

Отображение от аффинных эквивалентностей к их базовым функциям является инъективным.

LaTeX

$$$\forall e,e',\; (\forall x\; e(x)=e'(x)) \Rightarrow e=e'$$$

Lean4

theorem coeFn_injective : @Injective (P₁ ≃ᵃ[k] P₂) (P₁ → P₂) (⇑) :=
  DFunLike.coe_injective

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

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

Разделы

Аффилиация

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