inj_on_of_nodup_map — Mathlib

English

If map f l is nodup, then f is injective on l.

Русский

Если map f l без повторов, то f инъективна на множестве l.

LaTeX

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

Lean4

theorem inj_on_of_nodup_map {f : α → β} {l : List α} (d : Nodup (map f l)) :
    ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y := by
  induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
    simp only [mem_cons]
    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
    · rfl
    · apply (d.1 _ h₂ h₃.symm).elim
    · apply (d.1 _ h₁ h₃).elim
    · apply ih d.2 h₁ h₂ h₃

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