notMem_keys_kerase — Mathlib

English

If a1 ≠ a2, then a1 ∈ (kerase a2 l).keys is equivalent to a1 ∈ l.keys. This holds for any l.

Русский

Если a1 ≠ a2, то a1 принадлежит ключам kerase a2 l тогда и только тогда, когда a1 принадлежит ключам l.

LaTeX

$$∀ {α β} {l : List (Σ β)} {a1 a2}, a1 ≠ a2 → (a1 ∈ (kerase a2 l).keys ↔ a1 ∈ l.keys)$$

Lean4

@[simp]
theorem notMem_keys_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) : a ∉ (kerase a l).keys := by
  induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [nodupKeys_cons] at nd
    by_cases h : a = hd.1
    · subst h
      simp [nd.1]
    · simp [h, ih nd.2]

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