mathlib documentation

data.finset.sum

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 the finset.sum operation which computes the additive sum.

Main declarations #

def finset.disj_sum {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
finset β)

Disjoint sum of finsets.

Equations
@[simp]
theorem finset.val_disj_sum {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
@[simp]
theorem finset.empty_disj_sum {α : Type u_1} {β : Type u_2} (t : finset β) :
@[simp]
theorem finset.disj_sum_empty {α : Type u_1} {β : Type u_2} (s : finset α) :
@[simp]
theorem finset.card_disj_sum {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
(s.disj_sum t).card = s.card + t.card
theorem finset.mem_disj_sum {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {x : α β} :
x s.disj_sum t ( (a : α), a s sum.inl a = x) (b : β), b t sum.inr b = x
@[simp]
theorem finset.inl_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {a : α} :
@[simp]
theorem finset.inr_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {b : β} :
theorem finset.disj_sum_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disj_sum t₁ s₂.disj_sum t₂
theorem finset.disj_sum_mono_left {α : Type u_1} {β : Type u_2} (t : finset β) :
monotone (λ (s : finset α), s.disj_sum t)
theorem finset.disj_sum_mono_right {α : Type u_1} {β : Type u_2} (s : finset α) :
theorem finset.disj_sum_ssubset_disj_sum_of_ssubset_of_subset {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disj_sum t₁ s₂.disj_sum t₂
theorem finset.disj_sum_ssubset_disj_sum_of_subset_of_ssubset {α : Type u_1} {β : Type u_2} {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disj_sum t₁ s₂.disj_sum t₂
theorem finset.disj_sum_strict_mono_left {α : Type u_1} {β : Type u_2} (t : finset β) :
strict_mono (λ (s : finset α), s.disj_sum t)
theorem finset.disj_sum_strict_mono_right {α : Type u_1} {β : Type u_2} (s : finset α) :