extract_eq_lookup_erase — Mathlib

English

For any a : α and Finmap s, the extraction at a satisfies extract a s = (lookup a s, erase a s).

Русский

Для любого a : α и Finmap s выполняется extract a s = (lookup a s, erase a s).

LaTeX

$$$ \operatorname{extract}(a,s) = (\operatorname{lookup}(a,s), \operatorname{erase}(a,s)) $$$

Lean4

@[simp]
theorem extract_eq_lookup_erase (a : α) (s : Finmap β) : extract a s = (lookup a s, erase a s) :=
  induction_on s fun s => by simp [extract]

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