kunion — Mathlib

English

If l1 and l2 have NodupKeys, then their kunion also has NodupKeys; the combined key-set remains without duplicates.

Русский

Если у списков l1 и l2 нет повторяющихся ключей, то и их kunion без повторов ключей.

LaTeX

$$∀ {l1 l2}, l1.NodupKeys → l2.NodupKeys → (kunion l1 l2).NodupKeys$$

Lean4

theorem kunion (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) : (kunion l₁ l₂).NodupKeys := by
  induction l₁ generalizing l₂ with
  | nil => simp only [nil_kunion, nd₂]
  | cons s l₁ ih =>
    simp only [nodupKeys_cons] at nd₁
    simp [nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]

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