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 : Finset α) (t : Finset β) : Finset (α ⊕ β)

Disjoint sum of finsets.

Equations

• Finset.disjSum s t = { val := Multiset.disjSum s.val t.val, nodup := ⋯ }

@[simp]

theorem Finset.val_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : (Finset.disjSum s t).val = Multiset.disjSum s.val t.val

@[simp]

theorem Finset.empty_disjSum {α : Type u_1} {β : Type u_2} (t : Finset β) : Finset.disjSum ∅ t = Finset.map Function.Embedding.inr t

@[simp]

theorem Finset.disjSum_empty {α : Type u_1} {β : Type u_2} (s : Finset α) : Finset.disjSum s ∅ = Finset.map Function.Embedding.inl s

@[simp]

theorem Finset.card_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : (Finset.disjSum s t).card = s.card + t.card

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.disjUnion (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t) ⋯ = Finset.disjSum s t

theorem Finset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {x : α ⊕ β} : x ∈ Finset.disjSum s t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x

@[simp]

theorem Finset.inl_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {a : α} : Sum.inl a ∈ Finset.disjSum s t ↔ a ∈ s

@[simp]

theorem Finset.inr_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {b : β} : Sum.inr b ∈ Finset.disjSum s t ↔ b ∈ t

@[simp]

theorem Finset.disjSum_eq_empty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : Finset.disjSum s t = ∅ ↔ s = ∅ ∧ t = ∅

theorem Finset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : Finset.disjSum s₁ t₁ ⊆ Finset.disjSum s₂ t₂

theorem Finset.disjSum_mono_left {α : Type u_1} {β : Type u_2} (t : Finset β) : Monotone fun (s : Finset α) => Finset.disjSum s t

theorem Finset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : Finset α) : Monotone (Finset.disjSum s)

theorem Finset.disjSum_ssubset_disjSum_of_ssubset_of_subset {α : Type u_1} {β : Type u_2} {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (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₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊂ t₂) : Finset.disjSum s₁ t₁ ⊂ Finset.disjSum s₂ t₂

theorem Finset.disjSum_strictMono_left {α : Type u_1} {β : Type u_2} (t : Finset β) : StrictMono fun (s : Finset α) => Finset.disjSum s t

theorem Finset.disj_sum_strictMono_right {α : Type u_1} {β : Type u_2} (s : Finset α) : StrictMono (Finset.disjSum s)