Disjoint sum of finsets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the disjoint sum of two finsets as
finset (α ⊕ β). Beware not to confuse with
finset.sum operation which computes the additive sum.
Main declarations #
Disjoint sum of finsets.