English
For a zero-default total function, the support consists of inputs where the function value is nonzero; equivalently, it comes from the nonzero entries of the underlying data.
Русский
Для полной функции со значением по умолчанию равным нулю поддержка состоит из тех входов, на которых значение функции не равно нулю; эквивалентно не нулевым парам во входных данных.
LaTeX
$$$\mathrm{zeroDefaultSupp}(\mathrm{TotalFunction.withDefault}(A,a)) = \mathrm{List.toFinset}\Bigl((A\,\mathrm{dedupKeys}.\mathrm{filter}(\lambda ab, \; \Sigma\mathrm snd\; ab \neq 0))\;\mathrm{map} \; \Sigma.fst\Bigr)$$$
Lean4
/-- The support of a zero default `TotalFunction`. -/
@[simp]
def zeroDefaultSupp : TotalFunction α β → Finset α
| .withDefault A _ => List.toFinset <| (A.dedupKeys.filter fun ab => Sigma.snd ab ≠ 0).map Sigma.fst
