coeFn_inj

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

The map toEquiv: AffineEquiv → Equiv is injective.

Русский

Отображение toEquiv: AffineEquiv → Equiv инъективно.

LaTeX

$$$\text{toEquiv}$ is injective: \forall e,e',\; e.toEquiv = e'.toEquiv \Rightarrow e = e'$$$

Lean4

@[norm_cast]
theorem coeFn_inj {e e' : P₁ ≃ᵃ[k] P₂} : (e : P₁ → P₂) = e' ↔ e = e' := by simp

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

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

Разделы

Аффилиация

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