map_on — Mathlib

English

If a function f respects distinctness on a multiset, then mapping preserves Nodup.

Русский

Если функция f сохраняет различность на мультимножество, отображение сохраняет Nodup.

LaTeX

$$$\\forall f:\\\\alpha\\\\to\\\\beta$, (\\\\forall x\\\\in s\\\\,\\\\forall y\\\\in s, f x = f y \\\\Rightarrow x = y) \\\\Rightarrow \\\\mathrm{Nodup} s \\\\Rightarrow \\\\mathrm{Nodup}(\\\\mathrm{map} f s).$$$

Lean4

theorem map_on {f : α → β} : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Nodup s → Nodup (map f s) :=
  Quot.induction_on s fun _ => List.Nodup.map_on

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