Preparations for defining operations on Finset
. #
The operations here ignore multiplicities,
and preparatory for defining the corresponding operations on Finset
.
finset insert #
ndinsert a s
is the lift of the list insert
operation. This operation
does not respect multiplicities, unlike cons
, but it is suitable as
an insert operation on Finset
.
Instances For
finset union #
ndunion s t
is the lift of the list union
operation. This operation
does not respect multiplicities, unlike s ∪ t
, but it is suitable as
a union operation on Finset
. (s ∪ t
would also work as a union operation
on finset, but this is more efficient.)
Instances For
finset inter #
ndinter s t
is the lift of the list ∩
operation. This operation
does not respect multiplicities, unlike s ∩ t
, but it is suitable as
an intersection operation on Finset
. (s ∩ t
would also work as a union operation
on finset, but this is more efficient.)