toAffineEquiv_injective

Mathlib.Topology.Algebra.ContinuousAffineEquiv

URI: https://scilib.ai/kg/mathlib#ContinuousAffineEquiv.toAffineEquiv_injective

← MathLib Explorer

English

Same as before: the forgetful map toAffineEquiv is injective.

Русский

То же: инъекция у отображения toAffineEquiv.

LaTeX

$$$\\text{Injective}(\\text{toAffineEquiv})$$$

Lean4

theorem toAffineEquiv_injective : Injective (toAffineEquiv : (P₁ ≃ᴬ[k] P₂) → P₁ ≃ᵃ[k] P₂) :=
  by
  rintro ⟨e, econt, einv_cont⟩ ⟨e', e'cont, e'inv_cont⟩ H
  congr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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