keys_erase_toFinset — Mathlib

English

Erasing a in a Finmap corresponds to erasing a in its keys Finset.

Русский

Удаление ключа a из Finmap s соответствует удалению a из множества ключей Finset.

LaTeX

$$$\\operatorname{keys}(\\llbracket s\\rrbracket \\backslash a) = (\\operatorname{keys}(\\llbracket s \\rrbracket)) \\backslash a$$$

Lean4

@[simp]
theorem keys_erase_toFinset (a : α) (s : AList β) : keys ⟦s.erase a⟧ = (keys ⟦s⟧).erase a := by
  simp [Finset.erase, keys, AList.erase, keys_kerase]

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