nodup_map_iff_inj_on — Mathlib

English

Nodup (map f s) ↔ Nodup s when f is injective; equivalently, nodup on the map corresponds to nodup on the original set.

Русский

Nodup (map f s) ↔ Nodup s при инъективности f; эквивалентно тому, что Nodup на отображении соответствует Nodup на оригинале.

LaTeX

$$$\\forall {f : \\alpha \\\\to \\\\beta}, (Injective f) \\\\Rightarrow \\\\ Nodup (\\\\mathrm{map}\\\\ f\\\\ s) \\\\Leftrightarrow \\\\ Nodup s.$$$

Lean4

theorem nodup_map_iff_inj_on {f : α → β} {s : Multiset α} (d : Nodup s) :
    Nodup (map f s) ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
  ⟨inj_on_of_nodup_map, fun h => d.map_on h⟩

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