injective — Mathlib

English

If f is injective, then the induced map on Sym2 is injective: Injective (Sym2.map f).

Русский

Если f взаимно однозначно (инъективна), то отображение Sym2.map f инъективно: Injective (Sym2.map f).

LaTeX

$$$ \\text{Injective} \\, (\\mathrm{Sym2.map} \\, f) \quad\\text{given } \\text{Injective } f.$$$

Lean4

theorem injective {f : α → β} (hinj : Injective f) : Injective (map f) :=
  by
  intro z z'
  refine Sym2.inductionOn₂ z z' (fun x y x' y' => ?_)
  simp [hinj.eq_iff]

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