ofBijective — Mathlib

English

Bijective affine maps correspond to affine isomorphisms. In particular, any bijective affine map extends to an affine equivalence.

Русский

Биективные аффинные отображения соответствуют аффинным изоморфизмам. В частности, биективное аффинное отображение можно расширить до аффинного эквивалента.

LaTeX

$$$\exists e:\ P_1\simeq^a_k P_2\text{ with } e\text{ underlying }\phi \text{ and }\operatorname{Bijective}(\phi)$$$

Lean4

/-- Bijective affine maps are affine isomorphisms. -/
@[simps! linear apply]
noncomputable def ofBijective {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective φ) : P₁ ≃ᵃ[k] P₂ :=
  {
    Equiv.ofBijective _
      hφ with
    linear := LinearEquiv.ofBijective φ.linear (φ.linear_bijective_iff.mpr hφ)
    map_vadd' := φ.map_vadd }

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