toAList_keys_toFinset — Mathlib

English

For a finitely supported function f : α → M, the finite set of keys in its AList representation equals its support.

Русский

Для функции с конечной опорой f: α → M множество ключей в представлении AList равно её опоре.

LaTeX

$$$\\operatorname{Supp}(f) = \\{ i \\in \\alpha \\mid f(i) \\neq 0 \\}$$$

Lean4

@[simp]
theorem toAList_keys_toFinset [DecidableEq α] (f : α →₀ M) : f.toAList.keys.toFinset = f.support :=
  by
  ext
  simp [toAList, AList.keys, List.keys]

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