map_injective — Mathlib

English

If f is injective, then map f is injective on multisets: s.map f = t.map f implies s = t.

Русский

Если f инъективна, то отображение map f на мультимножества инъективно: s.map f = t.map f ⇒ s = t.

LaTeX

$$$\\forall {f: \\alpha \\to \\beta},\\; (Function.Injective f) \\to \\forall {s t: \\mathrm{Multiset}\\\\ \\alpha},\\\\ (s.map f) = (t.map f) \\\\Rightarrow s = t.$$$

Lean4

theorem map_injective {f : α → β} (hf : Function.Injective f) : Function.Injective (Multiset.map f) := fun _x _y =>
  (map_eq_map hf).1

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