bijective — Mathlib

English

If φ is injective, then the restriction is bijective between the source E and the image E.map φ.

Русский

Если φ инъективно, ограничение является биективным между E и E.map φ.

LaTeX

$$Bijective (restrict φ hEF) when φ is injective$$

Lean4

theorem bijective {E : AffineSubspace k P₁} [Nonempty E] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Injective φ) :
    Function.Bijective (φ.restrict (le_refl (E.map φ))) :=
  ⟨AffineMap.restrict.injective hφ _, AffineMap.restrict.surjective _ rfl⟩

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