erase_union_singleton — Mathlib

English

If s.lookup a = some b, then s.erase a ∪ singleton a b = s.

Русский

Если s.lookup a = some b, то s.erase a ∪ singleton a b = s.

LaTeX

$$$s.\\erase a \\cup \\{a \\mapsto b\\} = s$$$

Lean4

theorem erase_union_singleton (a : α) (b : β a) (s : Finmap β) (h : s.lookup a = some b) :
    s.erase a ∪ singleton a b = s :=
  ext_lookup fun x => by
    by_cases h' : x = a
    · subst a
      rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]
    · have : x ∉ singleton a b := by rwa [mem_singleton]
      rw [lookup_union_left_of_not_in this, lookup_erase_ne h']

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