map_on — Mathlib

English

If H holds that f is injective on l, then Nodup(l) implies Nodup(map f l).

Русский

Если ограничение H обеспечивает инъективность f на l, то из безповторности l следует безповторность map f l.

LaTeX

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

Lean4

theorem map_on {f : α → β} (H : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) (d : Nodup l) : (map f l).Nodup :=
  Pairwise.map _ (fun a b ⟨ma, mb, n⟩ e => n (H a ma b mb e)) (Pairwise.and_mem.1 d)

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