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 (Sum α β)

Disjoint sum of finsets.

Equations

• Eq (s.disjSum t) { val := s.val.disjSum t.val, nodup := ⋯ }

theorem Finset.val_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : Eq (s.disjSum t).val (s.val.disjSum t.val)

theorem Finset.empty_disjSum {α : Type u_1} {β : Type u_2} (t : Finset β) : Eq (EmptyCollection.emptyCollection.disjSum t) (map Function.Embedding.inr t)

theorem Finset.disjSum_empty {α : Type u_1} {β : Type u_2} (s : Finset α) : Eq (s.disjSum EmptyCollection.emptyCollection) (map Function.Embedding.inl s)

theorem Finset.card_disjSum {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : Eq (s.disjSum t).card (HAdd.hAdd 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)

theorem Finset.map_inl_disjUnion_map_inr {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : Eq ((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 : Sum α β} : Iff (Membership.mem (s.disjSum t) x) (Or (Exists fun (a : α) => And (Membership.mem s a) (Eq (Sum.inl a) x)) (Exists fun (b : β) => And (Membership.mem t b) (Eq (Sum.inr b) x)))

theorem Finset.inl_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {a : α} : Iff (Membership.mem (s.disjSum t) (Sum.inl a)) (Membership.mem s a)

theorem Finset.inr_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {b : β} : Iff (Membership.mem (s.disjSum t) (Sum.inr b)) (Membership.mem t b)

theorem Finset.disjSum_eq_empty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : Iff (Eq (s.disjSum t) EmptyCollection.emptyCollection) (And (Eq s EmptyCollection.emptyCollection) (Eq t EmptyCollection.emptyCollection))

theorem Finset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} (hs : HasSubset.Subset s₁ s₂) (ht : HasSubset.Subset t₁ t₂) : HasSubset.Subset (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 : HasSSubset.SSubset s₁ s₂) (ht : HasSubset.Subset t₁ t₂) : HasSSubset.SSubset (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 : HasSubset.Subset s₁ s₂) (ht : HasSSubset.SSubset t₁ t₂) : HasSSubset.SSubset (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

theorem Finset.disjSum_inj {α : Type u_4} {β : Type u_5} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} : Iff (Eq (s₁.disjSum t₁) (s₂.disjSum t₂)) (And (Eq s₁ s₂) (Eq 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 (Sum α β)) : 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

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

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

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

theorem Finset.mem_toLeft {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} {a : α} : Iff (Membership.mem u.toLeft a) (Membership.mem u (Sum.inl a))

theorem Finset.mem_toRight {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} {b : β} : Iff (Membership.mem u.toRight b) (Membership.mem u (Sum.inr b))

theorem Finset.toLeft_subset_toLeft {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} : HasSubset.Subset u v → HasSubset.Subset u.toLeft v.toLeft

theorem Finset.toRight_subset_toRight {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} : HasSubset.Subset u v → HasSubset.Subset 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 (Sum α β)} : Eq (u.toLeft.disjSum u.toRight) u

theorem Finset.card_toLeft_add_card_toRight {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} : Eq (HAdd.hAdd u.toLeft.card u.toRight.card) u.card

theorem Finset.card_toLeft_le {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} : LE.le u.toLeft.card u.card

theorem Finset.card_toRight_le {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} : LE.le u.toRight.card u.card

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

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

theorem Finset.disjSum_eq_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (Sum α β)} : Iff (Eq (s.disjSum t) u) (And (Eq s u.toLeft) (Eq t u.toRight))

theorem Finset.eq_disjSum_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (Sum α β)} : Iff (Eq u (s.disjSum t)) (And (Eq u.toLeft s) (Eq u.toRight t))

theorem Finset.disjSum_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (Sum α β)} : Iff (HasSubset.Subset (s.disjSum t) u) (And (HasSubset.Subset s u.toLeft) (HasSubset.Subset t u.toRight))

theorem Finset.subset_disjSum {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (Sum α β)} : Iff (HasSubset.Subset u (s.disjSum t)) (And (HasSubset.Subset u.toLeft s) (HasSubset.Subset u.toRight t))

theorem Finset.subset_map_inl {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (Sum α β)} : Iff (HasSubset.Subset u (map Function.Embedding.inl s)) (And (HasSubset.Subset u.toLeft s) (Eq u.toRight EmptyCollection.emptyCollection))

theorem Finset.subset_map_inr {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (Sum α β)} : Iff (HasSubset.Subset u (map Function.Embedding.inr t)) (And (Eq u.toLeft EmptyCollection.emptyCollection) (HasSubset.Subset u.toRight t))

theorem Finset.map_inl_subset_iff_subset_toLeft {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (Sum α β)} : Iff (HasSubset.Subset (map Function.Embedding.inl s) u) (HasSubset.Subset s u.toLeft)

theorem Finset.map_inr_subset_iff_subset_toRight {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (Sum α β)} : Iff (HasSubset.Subset (map Function.Embedding.inr t) u) (HasSubset.Subset 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

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

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

theorem Finset.toLeft_cons_inl {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} {a : α} (ha : Not (Membership.mem u (Sum.inl a))) : Eq (cons (Sum.inl a) u ha).toLeft (cons a u.toLeft ⋯)

theorem Finset.toLeft_cons_inr {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} {b : β} (hb : Not (Membership.mem u (Sum.inr b))) : Eq (cons (Sum.inr b) u hb).toLeft u.toLeft

theorem Finset.toRight_cons_inl {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} {a : α} (ha : Not (Membership.mem u (Sum.inl a))) : Eq (cons (Sum.inl a) u ha).toRight u.toRight

theorem Finset.toRight_cons_inr {α : Type u_1} {β : Type u_2} {u : Finset (Sum α β)} {b : β} (hb : Not (Membership.mem u (Sum.inr b))) : Eq (cons (Sum.inr b) u hb).toRight (cons b u.toRight ⋯)

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

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

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

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

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

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

theorem Finset.toLeft_inter {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} [DecidableEq α] [DecidableEq β] : Eq (Inter.inter u v).toLeft (Inter.inter u.toLeft v.toLeft)

theorem Finset.toRight_inter {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} [DecidableEq α] [DecidableEq β] : Eq (Inter.inter u v).toRight (Inter.inter u.toRight v.toRight)

theorem Finset.toLeft_union {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} [DecidableEq α] [DecidableEq β] : Eq (Union.union u v).toLeft (Union.union u.toLeft v.toLeft)

theorem Finset.toRight_union {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} [DecidableEq α] [DecidableEq β] : Eq (Union.union u v).toRight (Union.union u.toRight v.toRight)

theorem Finset.toLeft_sdiff {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} [DecidableEq α] [DecidableEq β] : Eq (SDiff.sdiff u v).toLeft (SDiff.sdiff u.toLeft v.toLeft)

theorem Finset.toRight_sdiff {α : Type u_1} {β : Type u_2} {u v : Finset (Sum α β)} [DecidableEq α] [DecidableEq β] : Eq (SDiff.sdiff u v).toRight (SDiff.sdiff u.toRight v.toRight)

def Finset.sumEquiv {α : Type u_4} {β : Type u_5} : OrderIso (Finset (Sum α β)) (Prod (Finset α) (Finset β))

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

Equations

• One or more equations did not get rendered due to their size.

theorem Finset.sumEquiv_apply_snd {α : Type u_4} {β : Type u_5} (s : Finset (Sum α β)) : Eq (DFunLike.coe sumEquiv s).snd s.toRight

theorem Finset.sumEquiv_apply_fst {α : Type u_4} {β : Type u_5} (s : Finset (Sum α β)) : Eq (DFunLike.coe sumEquiv s).fst s.toLeft

theorem Finset.sumEquiv_symm_apply {α : Type u_4} {β : Type u_5} (s : Prod (Finset α) (Finset β)) : Eq (DFunLike.coe sumEquiv.symm s) (s.fst.disjSum s.snd)

theorem Finset.map_disjSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : Finset β} (f : Function.Embedding (Sum α β) γ) : Eq (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 : Sum α β → γ) (b₁ b₂ : γ) (op : γ → γ → γ) [Std.Commutative op] [Std.Associative op] : Eq (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))