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.
• Finset.toLeft: Given a finset of elements α ⊕ β, extracts all the elements of the form α.
• Finset.toRight: Given a finset of elements α ⊕ β, extracts all the elements of the form β.

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 := ⋯ }

@[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 = map Function.Embedding.inr t

@[simp]

theorem Finset.disjSum_empty {α : Type u_1} {β : Type u_2} (s : Finset α) : s.disjSum ∅ = 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 (map Function.Embedding.inl s) (map Function.Embedding.inr t)

@[simp]

theorem Finset.map_inl_disjUnion_map_inr {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : (map Function.Embedding.inl s).disjUnion (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 ↔ (∃ 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 ∈ 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₁ s₂ : Finset α} {t₁ 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₁ s₂ : Finset α} {t₁ 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₁ s₂ : Finset α} {t₁ 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.disjSum_strictMono_right {α : Type u_1} {β : Type u_2} (s : Finset α) : StrictMono s.disjSum

@[simp]

theorem Finset.disjSum_inj {α : Type u_4} {β : Type u_5} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} : s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

theorem Finset.Injective2_disjSum {α : Type u_4} {β : Type u_5} : Function.Injective2 disjSum

def Finset.toLeft {α : Type u_1} {β : Type u_2} (u : 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

• u.toLeft = Finset.filterMap (Sum.elim some fun (x : β) => none) u ⋯

def Finset.toRight {α : Type u_1} {β : Type u_2} (u : 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

• u.toRight = Finset.filterMap (Sum.elim (fun (x : α) => none) some) u ⋯

@[simp]

theorem Finset.mem_toLeft {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} : a ∈ u.toLeft ↔ Sum.inl a ∈ u

@[simp]

theorem Finset.mem_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} : b ∈ u.toRight ↔ Sum.inr b ∈ u

theorem Finset.toLeft_subset_toLeft {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} : u ⊆ v → u.toLeft ⊆ v.toLeft

theorem Finset.toRight_subset_toRight {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} : u ⊆ v → u.toRight ⊆ v.toRight

theorem Finset.toLeft_monotone {α : Type u_1} {β : Type u_2} : Monotone toLeft

theorem Finset.toRight_monotone {α : Type u_1} {β : Type u_2} : Monotone toRight

theorem Finset.toLeft_disjSum_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : u.toLeft.disjSum u.toRight = u

theorem Finset.card_toLeft_add_card_toRight {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : u.toLeft.card + u.toRight.card = u.card

theorem Finset.card_toLeft_le {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : u.toLeft.card ≤ u.card

theorem Finset.card_toRight_le {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : u.toRight.card ≤ u.card

@[simp]

theorem Finset.toLeft_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : (s.disjSum t).toLeft = s

@[simp]

theorem Finset.toRight_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : (s.disjSum t).toRight = t

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

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

theorem Finset.disjSum_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)} : s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight

theorem Finset.subset_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)} : u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t

theorem Finset.subset_map_inl {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (α ⊕ β)} : u ⊆ map Function.Embedding.inl s ↔ u.toLeft ⊆ s ∧ u.toRight = ∅

theorem Finset.subset_map_inr {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (α ⊕ β)} : u ⊆ map Function.Embedding.inr t ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t

theorem Finset.map_inl_subset_iff_subset_toLeft {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (α ⊕ β)} : map Function.Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft

theorem Finset.map_inr_subset_iff_subset_toRight {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (α ⊕ β)} : map Function.Embedding.inr t ⊆ u ↔ t ⊆ u.toRight

theorem Finset.gc_map_inl_toLeft {α : Type u_1} {β : Type u_2} : GaloisConnection (fun (x : Finset α) => map Function.Embedding.inl x) toLeft

theorem Finset.gc_map_inr_toRight {α : Type u_1} {β : Type u_2} : GaloisConnection (fun (x : Finset β) => map Function.Embedding.inr x) toRight

@[simp]

theorem Finset.toLeft_map_sumComm {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

@[simp]

theorem Finset.toRight_map_sumComm {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

@[simp]

theorem Finset.toLeft_cons_inl {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} (ha : Sum.inl a ∉ u) : (cons (Sum.inl a) u ha).toLeft = cons a u.toLeft ⋯

@[simp]

theorem Finset.toLeft_cons_inr {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} (hb : Sum.inr b ∉ u) : (cons (Sum.inr b) u hb).toLeft = u.toLeft

@[simp]

theorem Finset.toRight_cons_inl {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} (ha : Sum.inl a ∉ u) : (cons (Sum.inl a) u ha).toRight = u.toRight

@[simp]

theorem Finset.toRight_cons_inr {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} (hb : Sum.inr b ∉ u) : (cons (Sum.inr b) u hb).toRight = cons b u.toRight ⋯

theorem Finset.toLeft_image_swap {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (image Sum.swap u).toLeft = u.toRight

theorem Finset.toRight_image_swap {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (image Sum.swap u).toRight = u.toLeft

@[simp]

theorem Finset.toLeft_insert_inl {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} [DecidableEq α] [DecidableEq β] : (insert (Sum.inl a) u).toLeft = insert a u.toLeft

@[simp]

theorem Finset.toLeft_insert_inr {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} [DecidableEq α] [DecidableEq β] : (insert (Sum.inr b) u).toLeft = u.toLeft

@[simp]

theorem Finset.toRight_insert_inl {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} [DecidableEq α] [DecidableEq β] : (insert (Sum.inl a) u).toRight = u.toRight

@[simp]

theorem Finset.toRight_insert_inr {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} [DecidableEq α] [DecidableEq β] : (insert (Sum.inr b) u).toRight = insert b u.toRight

theorem Finset.toLeft_inter {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

theorem Finset.toRight_inter {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (u ∩ v).toRight = u.toRight ∩ v.toRight

theorem Finset.toLeft_union {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

theorem Finset.toRight_union {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (u ∪ v).toRight = u.toRight ∪ v.toRight

theorem Finset.toLeft_sdiff {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (u \ v).toLeft = u.toLeft \ v.toLeft

theorem Finset.toRight_sdiff {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [DecidableEq α] [DecidableEq β] : (u \ v).toRight = u.toRight \ v.toRight

def Finset.sumEquiv {α : Type u_4} {β : Type u_5} : Finset (α ⊕ β) ≃o Finset α × Finset β

Finsets on sum types are equivalent to pairs of finsets on each summand.

Equations

• Finset.sumEquiv = { toFun := fun (s : Finset (α ⊕ β)) => (s.toLeft, s.toRight), invFun := fun (s : Finset α × Finset β) => s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Finset.sumEquiv_apply_snd {α : Type u_4} {β : Type u_5} (s : Finset (α ⊕ β)) : (sumEquiv s).2 = s.toRight

@[simp]

theorem Finset.sumEquiv_apply_fst {α : Type u_4} {β : Type u_5} (s : Finset (α ⊕ β)) : (sumEquiv s).1 = s.toLeft

@[simp]

theorem Finset.sumEquiv_symm_apply {α : Type u_4} {β : Type u_5} (s : Finset α × Finset β) : sumEquiv.symm s = s.1.disjSum s.2

theorem Finset.map_disjSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : Finset β} (f : α ⊕ β ↪ γ) : map f (s.disjSum t) = (map (Function.Embedding.inl.trans f) s).disjUnion (map (Function.Embedding.inr.trans f) t) ⋯

theorem Finset.fold_disjSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (t : Finset β) (f : α ⊕ β → γ) (b₁ b₂ : γ) (op : γ → γ → γ) [Std.Commutative op] [Std.Associative op] : fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun (x : α) => f (Sum.inl x)) s) (fold op b₂ (fun (x : β) => f (Sum.inr x)) t)