toAList_lookupFinsupp — Mathlib

English

The Finsupp obtained from the AList representation of f is f itself.

Русский

Finsupp, полученная из представления AList функции f, равна самой f.

LaTeX

$$$f\\mathrm{.toAList}.lookupFinsupp = f$$$

Lean4

@[simp]
theorem _root_.Finsupp.toAList_lookupFinsupp (f : α →₀ M) : f.toAList.lookupFinsupp = f :=
  by
  ext a
  classical
  by_cases h : f a = 0
  · suffices f.toAList.lookup a = none by simp [h, this]
    simp [lookup_eq_none, h]
  · suffices f.toAList.lookup a = some (f a) by simp [this]
    apply mem_lookup_iff.2
    simpa using h

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