toContinuousAffineMap_injective — Mathlib

English

The map that sends a continuous affine equivalence to its underlying continuous affine map is injective: if two such equivalences have the same underlying map, then they are equal.

Русский

Отображение, которое отправляет непрерывное аффинальное эквивалентное отображение к его базовой непрерывной аффинной карте, инъективно: если две такие эквивалентности имеют одинаковую базовую карту, то они равны.

LaTeX

$$$\forall e,e'.\ (\mathrm{toContinuousAffineMap}(e) = \mathrm{toContinuousAffineMap}(e')) \Rightarrow e = e'$$$

Lean4

theorem toContinuousAffineMap_injective : Function.Injective (toContinuousAffineMap : (P₁ ≃ᴬ[k] P₂) → (P₁ →ᴬ[k] P₂)) :=
  by
  intro e e' h
  ext p
  simp_rw [← coe_toContinuousAffineMap, h]

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