# Documentation

Mathlib.Data.Finset.Sum

# 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 of s and t.
def Finset.disjSum {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
Finset (α β)

Disjoint sum of finsets.

Equations
@[simp]
theorem Finset.val_disjSum {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
().val = Multiset.disjSum s.val t.val
@[simp]
theorem Finset.empty_disjSum {α : Type u_1} {β : Type u_2} (t : ) :
= Finset.map Function.Embedding.inr t
@[simp]
theorem Finset.disjSum_empty {α : Type u_1} {β : Type u_2} (s : ) :
= Finset.map Function.Embedding.inl s
@[simp]
theorem Finset.card_disjSum {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
=
theorem Finset.disjoint_map_inl_map_inr {α : Type u_2} {β : Type u_1} (s : ) (t : ) :
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 : ) (t : ) :
Finset.disjUnion (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t) (_ : Disjoint (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t)) =
theorem Finset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } {x : α β} :
x (a, a s = x) b, b t = x
@[simp]
theorem Finset.inl_mem_disjSum {α : Type u_2} {β : Type u_1} {s : } {t : } {a : α} :
a s
@[simp]
theorem Finset.inr_mem_disjSum {α : Type u_2} {β : Type u_1} {s : } {t : } {b : β} :
b t
theorem Finset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
Finset.disjSum s₁ t₁ Finset.disjSum s₂ t₂
theorem Finset.disjSum_mono_left {α : Type u_2} {β : Type u_1} (t : ) :
Monotone fun s =>
theorem Finset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : ) :
theorem Finset.disjSum_ssubset_disjSum_of_ssubset_of_subset {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
Finset.disjSum s₁ t₁ Finset.disjSum s₂ t₂
theorem Finset.disjSum_ssubset_disjSum_of_subset_of_ssubset {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
Finset.disjSum s₁ t₁ Finset.disjSum s₂ t₂
theorem Finset.disjSum_strictMono_left {α : Type u_2} {β : Type u_1} (t : ) :
StrictMono fun s =>
theorem Finset.disj_sum_strictMono_right {α : Type u_1} {β : Type u_2} (s : ) :