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 #

def Finset.disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
Finset (α β)

Disjoint sum of finsets.

Equations
  • s.disjSum t = { val := s.val.disjSum t.val, nodup := }
Instances For
    @[simp]
    theorem Finset.val_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
    (s.disjSum t).val = s.val.disjSum t.val
    @[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
    @[simp]
    theorem Finset.card_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
    (s.disjSum 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.map Function.Embedding.inl s).disjUnion (Finset.map Function.Embedding.inr t) = s.disjSum t
    theorem Finset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {x : α β} :
    x s.disjSum t (∃ as, Sum.inl a = x) bt, Sum.inr b = x
    @[simp]
    theorem Finset.inl_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {a : α} :
    Sum.inl a s.disjSum t a s
    @[simp]
    theorem Finset.inr_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {b : β} :
    Sum.inr b s.disjSum t b t
    @[simp]
    theorem Finset.disjSum_eq_empty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
    s.disjSum 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₂) :
    s₁.disjSum t₁ s₂.disjSum t₂
    theorem Finset.disjSum_mono_left {α : Type u_1} {β : Type u_2} (t : Finset β) :
    Monotone fun (s : Finset α) => s.disjSum t
    theorem Finset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : Finset α) :
    Monotone s.disjSum
    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₂) :
    s₁.disjSum t₁ s₂.disjSum 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₂) :
    s₁.disjSum 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