nodupKeys_dedupKeys — Mathlib

English

Applying dedupKeys to a list yields a list with NodupKeys; that is, the deduped list has no duplicate keys.

Русский

Применение dedupKeys к списку дает список без повторяющихся ключей.

LaTeX

$$NodupKeys (dedupKeys l)$$

Lean4

theorem nodupKeys_dedupKeys (l : List (Sigma β)) : NodupKeys (dedupKeys l) :=
  by
  dsimp [dedupKeys]
  generalize hl : nil = l'
  have : NodupKeys l' := by
    rw [← hl]
    apply nodup_nil
  clear hl
  induction l with
  | nil => apply this
  | cons x xs l_ih =>
    cases x
    simp only [foldr_cons, kinsert_def, nodupKeys_cons]
    constructor
    · simp only [keys_kerase]
      apply l_ih.not_mem_erase
    · exact l_ih.kerase _

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