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 #

source
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
    source
    @[simp]
    theorem Finset.val_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
    (s.disjSum t).val = s.val.disjSum t.val
    source
    @[simp]
    theorem Finset.empty_disjSum {α : Type u_1} {β : Type u_2} (t : Finset β) :
    ∅.disjSum t = Finset.map Function.Embedding.inr t
    source
    @[simp]
    theorem Finset.disjSum_empty {α : Type u_1} {β : Type u_2} (s : Finset α) :
    s.disjSum ∅ = Finset.map Function.Embedding.inl s
    source
    @[simp]
    theorem Finset.card_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
    (s.disjSum 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_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
    source
    theorem Finset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {x : α ⊕ β} :
    x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem Finset.disjSum_eq_empty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
    s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅
    source
    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₂
    source
    theorem Finset.disjSum_mono_left {α : Type u_1} {β : Type u_2} (t : Finset β) :
    Monotone fun (s : Finset α) => s.disjSum t
    source
    theorem Finset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : Finset α) :
    Monotone s.disjSum
    source
    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₂
    source
    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₂
    source
    theorem Finset.disjSum_strictMono_left {α : Type u_1} {β : Type u_2} (t : Finset β) :
    StrictMono fun (s : Finset α) => s.disjSum t
    source
    theorem Finset.disj_sum_strictMono_right {α : Type u_1} {β : Type u_2} (s : Finset α) :
    StrictMono s.disjSum
    source
    @[simp]
    theorem Finset.disjSum_inj {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} :
    s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂
    source
    theorem Finset.Injective2_disjSum {α : Type u_3} {β : Type u_4} :
    Function.Injective2 Finset.disjSum
    source
    def Finset.toLeft {α : Type u_1} {β : Type u_2} (s : Finset (α ⊕ β)) :
    Finset α

    Given a finset of elements α ⊕ β, extract all the elements of the form α. This forms a quasi-inverse to disjSum, in that it recovers its left input.

    See also List.partitionMap.

    Equations
    • s.toLeft = s.disjiUnion (Sum.elim singleton fun (x : β) => ∅) ⋯
    Instances For
      source
      def Finset.toRight {α : Type u_1} {β : Type u_2} (s : Finset (α ⊕ β)) :
      Finset β

      Given a finset of elements α ⊕ β, extract all the elements of the form β. This forms a quasi-inverse to disjSum, in that it recovers its right input.

      See also List.partitionMap.

      Equations
      • s.toRight = s.disjiUnion (Sum.elim (fun (x : α) => ∅) singleton) ⋯
      Instances For
        source
        @[simp]
        theorem Finset.mem_toLeft {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {x : α} :
        x ∈ u.toLeft ↔ Sum.inl x ∈ u
        source
        @[simp]
        theorem Finset.mem_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {x : β} :
        x ∈ u.toRight ↔ Sum.inr x ∈ u
        source
        theorem Finset.toLeft_subset_toLeft {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} :
        u ⊆ v → u.toLeft ⊆ v.toLeft
        source
        theorem Finset.toRight_subset_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} :
        u ⊆ v → u.toRight ⊆ v.toRight
        source
        theorem Finset.toLeft_monotone {α : Type u_1} {β : Type u_2} :
        Monotone Finset.toLeft
        source
        theorem Finset.toRight_monotone {α : Type u_1} {β : Type u_2} :
        Monotone Finset.toRight
        source
        theorem Finset.toLeft_disjSum_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} :
        u.toLeft.disjSum u.toRight = u
        source
        theorem Finset.card_toLeft_add_card_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} :
        u.toLeft.card + u.toRight.card = u.card
        source
        theorem Finset.card_toLeft_le {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} :
        u.toLeft.card ≤ u.card
        source
        theorem Finset.card_toRight_le {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} :
        u.toRight.card ≤ u.card
        source
        @[simp]
        theorem Finset.toLeft_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
        (s.disjSum t).toLeft = s
        source
        @[simp]
        theorem Finset.toRight_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
        (s.disjSum t).toRight = t
        source
        theorem Finset.disjSum_eq_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)} :
        s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight
        source
        theorem Finset.eq_disjSum_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)} :
        u = s.disjSum t ↔ u.toLeft = s ∧ u.toRight = t
        source
        @[simp]
        theorem Finset.toLeft_map_sumComm {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} :
        (Finset.map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight
        source
        @[simp]
        theorem Finset.toRight_map_sumComm {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} :
        (Finset.map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft
        source
        @[simp]
        theorem Finset.toLeft_cons_inl {α : Type u_1} {β : Type u_2} {a : α} {u : Finset (α ⊕ β)} (ha : Sum.inl a ∉ u) :
        (Finset.cons (Sum.inl a) u ha).toLeft = Finset.cons a u.toLeft ⋯
        source
        @[simp]
        theorem Finset.toLeft_cons_inr {α : Type u_1} {β : Type u_2} {b : β} {u : Finset (α ⊕ β)} (hb : Sum.inr b ∉ u) :
        (Finset.cons (Sum.inr b) u hb).toLeft = u.toLeft
        source
        @[simp]
        theorem Finset.toRight_cons_inl {α : Type u_1} {β : Type u_2} {a : α} {u : Finset (α ⊕ β)} (ha : Sum.inl a ∉ u) :
        (Finset.cons (Sum.inl a) u ha).toRight = u.toRight
        source
        @[simp]
        theorem Finset.toRight_cons_inr {α : Type u_1} {β : Type u_2} {b : β} {u : Finset (α ⊕ β)} (hb : Sum.inr b ∉ u) :
        (Finset.cons (Sum.inr b) u hb).toRight = Finset.cons b u.toRight ⋯
        source
        theorem Finset.toLeft_image_swap {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (Finset.image Sum.swap u).toLeft = u.toRight
        source
        theorem Finset.toRight_image_swap {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (Finset.image Sum.swap u).toRight = u.toLeft
        source
        @[simp]
        theorem Finset.toLeft_insert_inl {α : Type u_1} {β : Type u_2} {a : α} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (insert (Sum.inl a) u).toLeft = insert a u.toLeft
        source
        @[simp]
        theorem Finset.toLeft_insert_inr {α : Type u_1} {β : Type u_2} {b : β} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (insert (Sum.inr b) u).toLeft = u.toLeft
        source
        @[simp]
        theorem Finset.toRight_insert_inl {α : Type u_1} {β : Type u_2} {a : α} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (insert (Sum.inl a) u).toRight = u.toRight
        source
        @[simp]
        theorem Finset.toRight_insert_inr {α : Type u_1} {β : Type u_2} {b : β} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (insert (Sum.inr b) u).toRight = insert b u.toRight
        source
        theorem Finset.toLeft_inter {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (u ∩ v).toLeft = u.toLeft ∩ v.toLeft
        source
        theorem Finset.toRight_inter {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (u ∩ v).toRight = u.toRight ∩ v.toRight
        source
        theorem Finset.toLeft_union {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (u ∪ v).toLeft = u.toLeft ∪ v.toLeft
        source
        theorem Finset.toRight_union {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (u ∪ v).toRight = u.toRight ∪ v.toRight
        source
        theorem Finset.toLeft_sdiff {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (u \ v).toLeft = u.toLeft \ v.toLeft
        source
        theorem Finset.toRight_sdiff {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] :
        (u \ v).toRight = u.toRight \ v.toRight