lookupFinsupp_support — Mathlib

English

The support of l.lookupFinsupp equals the indices where l has nonzero values.

Русский

Опора функции $\\mathrm{lookupFinsupp}$ равна множеству индексов, на которых $l$ принимает ненулевые значения.

LaTeX

$$$\\operatorname{Supp}(l.lookupFinsupp) = \\{ i \\in \\alpha \\mid l(i) \\neq 0 \\}$$$

Lean4

@[simp]
theorem lookupFinsupp_support [DecidableEq α] [DecidableEq M] (l : AList fun _x : α => M) :
    l.lookupFinsupp.support = (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset :=
  by
  dsimp only [lookupFinsupp]
  congr!

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