map_eq_map — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_eq_map {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : s.map f = t.map f ↔ s = t :=
  by
  rw [← rel_eq, ← rel_eq, rel_map]
  simp only [hf.eq_iff]

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