Finitely supported functions on exactly one point #
This file contains definitions and basic results on defining/updating/removing Finsupp
s
using one point of the domain.
Main declarations #
Finsupp.single
: TheFinsupp
which is nonzero in exactly one point.Finsupp.update
: Changes one value of aFinsupp
.Finsupp.erase
: Replaces one value of aFinsupp
by0
.
Implementation notes #
This file is a noncomputable theory
and uses classical logic throughout.
single a b
is the finitely supported function with value b
at a
and zero otherwise.
Equations
Instances For
Finsupp.single a b
is injective in b
. For the statement that it is injective in a
, see
Finsupp.single_left_injective
Finsupp.single a b
is injective in a
. For the statement that it is injective in b
, see
Finsupp.single_injective
Replace the value of a α →₀ M
at a given point a : α
by a given value b : M
.
If b = 0
, this amounts to removing a
from the Finsupp.support
.
Otherwise, if a
was not in the Finsupp.support
, it is added to it.
This is the finitely-supported version of Function.update
.
Equations
Instances For
Alias of Finsupp.erase_of_notMem_support
.