map_injective — Mathlib

English

If f is injective, then map f is injective on each Sym α n.

Русский

Если f — инъективно, то map f инъективно на каждом Sym α n.

LaTeX

$$$\\forall f : \\alpha \\to \\beta,\\ \\operatorname{Injective}(f) \\Rightarrow \\forall n, \\operatorname{Injective}(\\mathrm{Sym.map}(f) : \\mathrm{Sym}(\\alpha,n) \\to \\mathrm{Sym}(\\beta,n)).$$$

Lean4

theorem map_injective {f : α → β} (hf : Injective f) (n : ℕ) : Injective (map f : Sym α n → Sym β n) := fun _ _ h =>
  coe_injective <| Multiset.map_injective hf <| coe_inj.2 h

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