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.disjSum
:s.disjSum t
is the disjoint sum ofs
andt
.
@[simp]
theorem
Finset.empty_disjSum
{α : Type u_1}
{β : Type u_2}
(t : Finset β)
:
∅.disjSum t = Finset.map Function.Embedding.inr t
@[simp]
theorem
Finset.disjSum_empty
{α : Type u_1}
{β : Type u_2}
(s : Finset α)
:
s.disjSum ∅ = Finset.map Function.Embedding.inl s
theorem
Finset.disjoint_map_inl_map_inr
{α : Type u_1}
{β : Type u_2}
(s : Finset α)
(t : Finset β)
:
Disjoint (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t)
@[simp]
theorem
Finset.map_inl_disjUnion_map_inr
{α : Type u_1}
{β : Type u_2}
(s : Finset α)
(t : Finset β)
:
(Finset.map Function.Embedding.inl s).disjUnion (Finset.map Function.Embedding.inr t) ⋯ = s.disjSum t
theorem
Finset.disjSum_strictMono_left
{α : Type u_1}
{β : Type u_2}
(t : Finset β)
:
StrictMono fun (s : Finset α) => s.disjSum t
theorem
Finset.disj_sum_strictMono_right
{α : Type u_1}
{β : Type u_2}
(s : Finset α)
:
StrictMono s.disjSum