keys_kerase — Mathlib

English

The keys of the list obtained after kerasing an element equal the original keys with that key erased. In symbols, (kerase a l).keys = l.keys.erase a.

Русский

Ключи списка, полученного после удаления элемента, равны ключам исходного списка с удалением данного ключа.

LaTeX

$$$\forall {a} {l : List (\Sigma \beta)}, (kerase\ a\ l).keys = l.keys.erase\ a$$$

Lean4

theorem keys_kerase {a} {l : List (Sigma β)} : (kerase a l).keys = l.keys.erase a :=
  by
  rw [keys, kerase, erase_eq_eraseP, eraseP_map, Function.comp_def]
  congr

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