Disjoint sum of finsets #
This file defines the disjoint sum of two finsets as finset (α ⊕ β)
. Beware not to confuse with
the finset.sum
operation which computes the additive sum.
Main declarations #
finset.disj_sum
:s.disj_sum t
is the disjoint sum ofs
andt
.
@[simp]
@[simp]
theorem
finset.disj_sum_strict_mono_left
{α : Type u_1}
{β : Type u_2}
(t : finset β) :
strict_mono (λ (s : finset α), s.disj_sum t)