nodup_map_iff_inj_on — Mathlib

English

Nodup(map f l) holds iff the function f is injective on l.

Русский

Безповторность map f l эквивалентна инъективности f на l.

LaTeX

$$$\\operatorname{Nodup}(\\operatorname{map} f l) \\iff \\forall x \\in l, \\forall y \\in l, f x = f y \\rightarrow x = y$$$

Lean4

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

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