injective — Mathlib

English

If φ is injective, then its restriction to E is injective (on the appropriate subtype).

Русский

Если φ инъективно, то ограничение φ на E инъективно.

LaTeX

$$$ \\text{injective}(\\phi.restrict hEF) $ given $\\text{injective}(\\phi) $$$

Lean4

theorem injective {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Injective φ) {E : AffineSubspace k P₁} {F : AffineSubspace k P₂}
    [Nonempty E] [Nonempty F] (hEF : E.map φ ≤ F) : Function.Injective (AffineMap.restrict φ hEF) :=
  by
  intro x y h
  simp only [Subtype.ext_iff, AffineMap.restrict.coe_apply] at h ⊢
  exact hφ h

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