mathlib3 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 #

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

Disjoint sum of finsets.

Equations
source
@[simp]
theorem finset.val_disj_sum {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
(s.disj_sum t).val = s.val.disj_sum t.val
source
@[simp]
theorem finset.empty_disj_sum {α : Type u_1} {β : Type u_2} (t : finset β) :
∅.disj_sum t = finset.map function.embedding.inr t
source
@[simp]
theorem finset.disj_sum_empty {α : Type u_1} {β : Type u_2} (s : finset α) :
s.disj_sum ∅ = finset.map function.embedding.inl s
source
@[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
source
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)
source
@[simp]
theorem finset.map_inl_disj_union_map_inr {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
(finset.map function.embedding.inl s).disj_union (finset.map function.embedding.inr t) _ = s.disj_sum t
source
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
source
@[simp]
theorem finset.inl_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {a : α} :
sum.inl a ∈ s.disj_sum t ↔ a ∈ s
source
@[simp]
theorem finset.inr_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {b : β} :
sum.inr b ∈ s.disj_sum t ↔ b ∈ t
source
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₂
source
theorem finset.disj_sum_mono_left {α : Type u_1} {β : Type u_2} (t : finset β) :
monotone (λ (s : finset α), s.disj_sum t)
source
theorem finset.disj_sum_mono_right {α : Type u_1} {β : Type u_2} (s : finset α) :
monotone s.disj_sum
source
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₂
source
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₂
source
theorem finset.disj_sum_strict_mono_left {α : Type u_1} {β : Type u_2} (t : finset β) :
strict_mono (λ (s : finset α), s.disj_sum t)
source
theorem finset.disj_sum_strict_mono_right {α : Type u_1} {β : Type u_2} (s : finset α) :
strict_mono s.disj_sum