Mathlib.Data.Finset.Sum

Finset.disjSum definition

: Finset (α ⊕ β)

Full source

/-- Disjoint sum of finsets. -/
def disjSum : Finset (α ⊕ β) :=
  ⟨s.1.disjSum t.1, s.2.disjSum t.2⟩

Disjoint sum of finite sets

Informal description

The disjoint sum of two finite sets $s$ over $\alpha$ and $t$ over $\beta$ is the finite set over the disjoint union $\alpha \oplus \beta$ obtained by taking the union of the image of $s$ under the left inclusion map $\text{inl}$ and the image of $t$ under the right inclusion map $\text{inr}$.

Finset.val_disjSum theorem

: (s.disjSum t).1 = s.1.disjSum t.1

Full source

@[simp]
theorem val_disjSum : (s.disjSum t).1 = s.1.disjSum t.1 :=
  rfl

Underlying Multiset of Disjoint Sum Equals Disjoint Sum of Underlying Multisets

Informal description

For any finite sets $s$ over type $\alpha$ and $t$ over type $\beta$, the underlying multiset of their disjoint sum $s.disjSum t$ is equal to the disjoint sum of the underlying multisets of $s$ and $t$.

Finset.empty_disjSum theorem

: (∅ : Finset α).disjSum t = t.map Embedding.inr

Full source

@[simp]
theorem empty_disjSum : (∅ : Finset α).disjSum t = t.map Embedding.inr :=
  val_inj.1 <| Multiset.zero_disjSum _

Disjoint Sum with Empty Left Finite Set Yields Right Inclusion Image

Informal description

For any finite set $t$ over type $\beta$, the disjoint sum of the empty finite set over $\alpha$ and $t$ is equal to the image of $t$ under the right inclusion map $\text{inr}$, i.e., $\emptyset \uplus t = \text{inr}(t)$.

Finset.disjSum_empty theorem

: s.disjSum (∅ : Finset β) = s.map Embedding.inl

Full source

@[simp]
theorem disjSum_empty : s.disjSum (∅ : Finset β) = s.map Embedding.inl :=
  val_inj.1 <| Multiset.disjSum_zero _

Disjoint sum with empty set yields left inclusion image

Informal description

For any finite set $s$ over a type $\alpha$, the disjoint sum of $s$ with the empty finite set over $\beta$ is equal to the image of $s$ under the left inclusion map $\text{inl} : \alpha \hookrightarrow \alpha \oplus \beta$. In symbols: $s \uplus \emptyset = \text{inl}(s)$.

Finset.card_disjSum theorem

: (s.disjSum t).card = s.card + t.card

Full source

@[simp]
theorem card_disjSum : (s.disjSum t).card = s.card + t.card :=
  Multiset.card_disjSum _ _

Cardinality of Disjoint Sum of Finite Sets: $|s \uplus t| = |s| + |t|$

Informal description

For any finite sets $s$ (of type $\alpha$) and $t$ (of type $\beta$), the cardinality of their disjoint sum $s \uplus t$ is equal to the sum of their cardinalities, i.e., $|s \uplus t| = |s| + |t|$.

Finset.disjoint_map_inl_map_inr theorem

: Disjoint (s.map Embedding.inl) (t.map Embedding.inr)

Full source

theorem disjoint_map_inl_map_inr : Disjoint (s.map Embedding.inl) (t.map Embedding.inr) := by
  simp_rw [disjoint_left, mem_map]
  rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩

Disjointness of Left and Right Inclusion Images in Sum Type

Informal description

For any finite sets $s$ (of type $\alpha$) and $t$ (of type $\beta$), the images of $s$ under the left inclusion map $\text{inl} : \alpha \hookrightarrow \alpha \oplus \beta$ and of $t$ under the right inclusion map $\text{inr} : \beta \hookrightarrow \alpha \oplus \beta$ are disjoint. In symbols: $\text{inl}(s) \cap \text{inr}(t) = \emptyset$.

Finset.map_inl_disjUnion_map_inr theorem

: (s.map Embedding.inl).disjUnion (t.map Embedding.inr) (disjoint_map_inl_map_inr _ _) = s.disjSum t

Full source

@[simp]
theorem map_inl_disjUnion_map_inr :
    (s.map Embedding.inl).disjUnion (t.map Embedding.inr) (disjoint_map_inl_map_inr _ _) =
      s.disjSum t :=
  rfl

Disjoint Union of Inclusion Maps Equals Disjoint Sum of Finite Sets

Informal description

For any finite sets $s$ (of type $\alpha$) and $t$ (of type $\beta$), the disjoint union of the image of $s$ under the left inclusion map $\text{inl} : \alpha \hookrightarrow \alpha \oplus \beta$ and the image of $t$ under the right inclusion map $\text{inr} : \beta \hookrightarrow \alpha \oplus \beta$ is equal to the disjoint sum $s \uplus t$ of $s$ and $t$. In symbols: $$(\text{inl}(s)) \uplus (\text{inr}(t)) = s \uplus t$$

Finset.mem_disjSum theorem

: x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Full source

theorem mem_disjSum : x ∈ s.disjSum tx ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x :=
  Multiset.mem_disjSum

Membership Criterion for Disjoint Sum of Finite Sets

Informal description

An element $x$ belongs to the disjoint sum $s \uplus t$ of finite sets $s$ and $t$ if and only if either there exists an element $a \in s$ such that $x = \text{inl}(a)$, or there exists an element $b \in t$ such that $x = \text{inr}(b)$. In symbols: $$x \in s \uplus t \leftrightarrow (\exists a \in s, x = \text{inl}(a)) \lor (\exists b \in t, x = \text{inr}(b))$$

Finset.inl_mem_disjSum theorem

: inl a ∈ s.disjSum t ↔ a ∈ s

Full source

@[simp]
theorem inl_mem_disjSum : inlinl a ∈ s.disjSum tinl a ∈ s.disjSum t ↔ a ∈ s :=
  Multiset.inl_mem_disjSum

Membership of Left Inclusion in Disjoint Sum of Finite Sets

Informal description

For any finite set $s$ over type $\alpha$, finite set $t$ over type $\beta$, and element $a \in \alpha$, the left inclusion $\text{inl}(a)$ is an element of the disjoint sum $s \uplus t$ if and only if $a$ is an element of $s$. In symbols: $$\text{inl}(a) \in s \uplus t \leftrightarrow a \in s$$

Finset.inr_mem_disjSum theorem

: inr b ∈ s.disjSum t ↔ b ∈ t

Full source

@[simp]
theorem inr_mem_disjSum : inrinr b ∈ s.disjSum tinr b ∈ s.disjSum t ↔ b ∈ t :=
  Multiset.inr_mem_disjSum

Membership of Right Inclusion in Disjoint Sum: $\text{inr}(b) \in s \uplus t \leftrightarrow b \in t$

Informal description

For any finite set $s$ over type $\alpha$, finite set $t$ over type $\beta$, and element $b \in \beta$, the right inclusion $\text{inr}(b)$ belongs to the disjoint sum $s \uplus t$ if and only if $b$ belongs to $t$. In symbols: $$\text{inr}(b) \in s \uplus t \leftrightarrow b \in t$$

Finset.disjSum_eq_empty theorem

: s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Full source

@[simp]
theorem disjSum_eq_empty : s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅ := by simp [Finset.ext_iff]

Disjoint Sum is Empty iff Both Sets Are Empty

Informal description

The disjoint sum of two finite sets $s \subseteq \alpha$ and $t \subseteq \beta$ is empty if and only if both $s$ and $t$ are empty, i.e., $$ s \uplus t = \emptyset \leftrightarrow s = \emptyset \land t = \emptyset $$ where $\uplus$ denotes the disjoint sum operation.

Finset.disjSum_mono theorem

(hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁.disjSum t₁ ⊆ s₂.disjSum t₂

Full source

theorem disjSum_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁.disjSum t₁ ⊆ s₂.disjSum t₂ :=
  val_le_iff.1 <| Multiset.disjSum_mono (val_le_iff.2 hs) (val_le_iff.2 ht)

Monotonicity of Disjoint Sum for Finite Sets

Informal description

For any finite sets $s₁, s₂$ of type $\alpha$ and $t₁, t₂$ of type $\beta$, if $s₁ \subseteq s₂$ and $t₁ \subseteq t₂$, then the disjoint sum $s₁.disjSum t₁$ is a subset of the disjoint sum $s₂.disjSum t₂$ in the finite set over $\alpha \oplus \beta$.

Finset.disjSum_mono_left theorem

(t : Finset β) : Monotone fun s : Finset α => s.disjSum t

Full source

theorem disjSum_mono_left (t : Finset β) : Monotone fun s : Finset α => s.disjSum t :=
  fun _ _ hs => disjSum_mono hs Subset.rfl

Monotonicity of Left Disjoint Sum Operation

Informal description

For any finite set $t$ of type $\beta$, the function $s \mapsto s \uplus t$ from finite subsets of $\alpha$ to finite subsets of $\alpha \oplus \beta$ is monotone. That is, for any finite sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subseteq s_2$, then $s_1 \uplus t \subseteq s_2 \uplus t$.

Finset.disjSum_mono_right theorem

(s : Finset α) : Monotone (s.disjSum : Finset β → Finset (α ⊕ β))

Full source

theorem disjSum_mono_right (s : Finset α) : Monotone (s.disjSum : Finset β → Finset (α ⊕ β)) :=
  fun _ _ => disjSum_mono Subset.rfl

Monotonicity of Disjoint Sum in the Right Argument

Informal description

For any finite set $s$ of type $\alpha$, the function $t \mapsto s.\text{disjSum}\, t$ is monotone with respect to the subset relation on finite sets of type $\beta$. That is, for any finite sets $t_1, t_2 \subseteq \beta$, if $t_1 \subseteq t_2$, then $s.\text{disjSum}\, t_1 \subseteq s.\text{disjSum}\, t_2$.

Finset.disjSum_ssubset_disjSum_of_ssubset_of_subset theorem

(hs : s₁ ⊂ s₂) (ht : t₁ ⊆ t₂) : s₁.disjSum t₁ ⊂ s₂.disjSum t₂

Full source

theorem disjSum_ssubset_disjSum_of_ssubset_of_subset (hs : s₁ ⊂ s₂) (ht : t₁ ⊆ t₂) :
    s₁.disjSum t₁ ⊂ s₂.disjSum t₂ :=
  val_lt_iff.1 <| disjSum_lt_disjSum_of_lt_of_le (val_lt_iff.2 hs) (val_le_iff.2 ht)

Strict Monotonicity of Disjoint Sum under Left-Strict and Right-Weak Subset Conditions

Informal description

For any finite sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, if $s_1$ is a strict subset of $s_2$ and $t_1$ is a subset of $t_2$, then the disjoint sum $s_1 \uplus t_1$ is a strict subset of the disjoint sum $s_2 \uplus t_2$.

Finset.disjSum_ssubset_disjSum_of_subset_of_ssubset theorem

(hs : s₁ ⊆ s₂) (ht : t₁ ⊂ t₂) : s₁.disjSum t₁ ⊂ s₂.disjSum t₂

Full source

theorem disjSum_ssubset_disjSum_of_subset_of_ssubset (hs : s₁ ⊆ s₂) (ht : t₁ ⊂ t₂) :
    s₁.disjSum t₁ ⊂ s₂.disjSum t₂ :=
  val_lt_iff.1 <| disjSum_lt_disjSum_of_le_of_lt (val_le_iff.2 hs) (val_lt_iff.2 ht)

Strict Subset Preservation under Disjoint Sum with Subset and Strict Subset Conditions

Informal description

For any finite sets $s_1, s_2$ over type $\alpha$ and $t_1, t_2$ over type $\beta$, if $s_1$ is a subset of $s_2$ and $t_1$ is a strict subset of $t_2$, then the disjoint sum $s_1 \uplus t_1$ is a strict subset of the disjoint sum $s_2 \uplus t_2$.

Finset.disjSum_strictMono_left theorem

(t : Finset β) : StrictMono fun s : Finset α => s.disjSum t

Full source

theorem disjSum_strictMono_left (t : Finset β) : StrictMono fun s : Finset α => s.disjSum t :=
  fun _ _ hs => disjSum_ssubset_disjSum_of_ssubset_of_subset hs Subset.rfl

Strict Monotonicity of Disjoint Sum in the Left Argument

Informal description

For any finite set $t$ over type $\beta$, the function that maps a finite set $s$ over type $\alpha$ to the disjoint sum $s \uplus t$ is strictly monotone. That is, for any finite sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subset s_2$, then $s_1 \uplus t \subset s_2 \uplus t$.

Finset.disj_sum_strictMono_right theorem

(s : Finset α) : StrictMono (s.disjSum : Finset β → Finset (α ⊕ β))

Full source

theorem disj_sum_strictMono_right (s : Finset α) :
    StrictMono (s.disjSum : Finset β → Finset (α ⊕ β)) := fun _ _ =>
  disjSum_ssubset_disjSum_of_subset_of_ssubset Subset.rfl

Strict Monotonicity of Right Disjoint Sum Operation

Informal description

For any finite set $s$ of type $\alpha$, the function $t \mapsto s \uplus t$ is strictly monotone with respect to the subset relation on finite sets of type $\beta$. That is, for any finite sets $t_1, t_2 \subseteq \beta$, if $t_1 \subset t_2$, then $s \uplus t_1 \subset s \uplus t_2$.

Finset.disjSum_inj theorem

 {α β : Type*} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} : s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Full source

@[simp] lemma disjSum_inj {α β : Type*} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} :
    s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂ := by
  simp [Finset.ext_iff]

Injectivity of Disjoint Sum of Finite Sets

Informal description

For any finite sets $s_1, s_2$ over type $\alpha$ and $t_1, t_2$ over type $\beta$, the disjoint sums $s_1.\text{disjSum}\, t_1$ and $s_2.\text{disjSum}\, t_2$ are equal if and only if $s_1 = s_2$ and $t_1 = t_2$.

Finset.Injective2_disjSum theorem

{α β : Type*} : Function.Injective2 (@disjSum α β)

Full source

lemma Injective2_disjSum {α β : Type*} : Function.Injective2 (@disjSum α β) :=
  fun _ _ _ _ => by simp [Finset.ext_iff]

Injectivity of Disjoint Sum Operation on Finite Sets

Informal description

For any types $\alpha$ and $\beta$, the disjoint sum operation on finite sets is injective in both arguments. That is, for any finite sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, if $s_1.\text{disjSum}\, t_1 = s_2.\text{disjSum}\, t_2$, then $s_1 = s_2$ and $t_1 = t_2$.

Finset.toLeft definition

(u : Finset (α ⊕ β)) : Finset α

Full source

/--
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`.
-/
def toLeft (u : Finset (α ⊕ β)) : Finset α :=
  u.filterMap (Sum.elim some fun _ => none) (by clear x; aesop)

Extraction of left components from a disjoint sum finite set

Informal description

Given a finite set $ u $ of elements of type $ \alpha \oplus \beta $, the function extracts all elements of the form $ \alpha $ (i.e., those constructed with `Sum.inl`). This operation forms a quasi-inverse to the disjoint sum operation, as it recovers the left input of the disjoint sum. In notation, $ \text{toLeft}(u) $ is the finite set $\{a : \alpha \mid \text{inl } a \in u\}$.

Finset.toRight definition

(u : Finset (α ⊕ β)) : Finset β

Full source

/--
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`.
-/
def toRight (u : Finset (α ⊕ β)) : Finset β :=
  u.filterMap (Sum.elim (fun _ => none) some) (by clear x; aesop)

Extraction of right components from a disjoint sum finite set

Informal description

Given a finite set $ u $ of elements of type $ \alpha \oplus \beta $, the function extracts all elements of the form $ \beta $ (i.e., those constructed with `Sum.inr`). This operation forms a quasi-inverse to the disjoint sum operation, as it recovers the right input of the disjoint sum. In notation, $ \text{toRight}(u) $ is the finite set $\{b : \beta \mid \text{inr } b \in u\}$.

Finset.mem_toLeft theorem

: a ∈ u.toLeft ↔ .inl a ∈ u

Full source

@[simp] lemma mem_toLeft : a ∈ u.toLefta ∈ u.toLeft ↔ .inl a ∈ u := by simp [toLeft]

Membership in Left Component Extraction of Disjoint Sum Finite Set

Informal description

For any element $a$ of type $\alpha$ and any finite set $u$ of elements of type $\alpha \oplus \beta$, the element $a$ belongs to the left component extraction $\text{toLeft}(u)$ if and only if the left injection $\text{inl } a$ belongs to $u$.

Finset.mem_toRight theorem

: b ∈ u.toRight ↔ .inr b ∈ u

Full source

@[simp] lemma mem_toRight : b ∈ u.toRightb ∈ u.toRight ↔ .inr b ∈ u := by simp [toRight]

Membership in Right Component Extraction of Disjoint Sum Finite Set

Informal description

For any element $b$ of type $\beta$ and any finite set $u$ of elements of type $\alpha \oplus \beta$, the element $b$ belongs to the right component extraction $\text{toRight}(u)$ if and only if the right injection $\text{inr } b$ belongs to $u$.

Finset.toLeft_subset_toLeft theorem

: u ⊆ v → u.toLeft ⊆ v.toLeft

Full source

@[gcongr]
lemma toLeft_subset_toLeft : u ⊆ v → u.toLeft ⊆ v.toLeft :=
  fun h _ => by simpa only [mem_toLeft] using @h _

Monotonicity of Left Component Extraction in Disjoint Sum Finite Sets

Informal description

For any two finite sets $u$ and $v$ of elements of type $\alpha \oplus \beta$, if $u$ is a subset of $v$, then the left component extraction of $u$ is a subset of the left component extraction of $v$. In other words, if $u \subseteq v$, then $\text{toLeft}(u) \subseteq \text{toLeft}(v)$.

Finset.toRight_subset_toRight theorem

: u ⊆ v → u.toRight ⊆ v.toRight

Full source

@[gcongr]
lemma toRight_subset_toRight : u ⊆ v → u.toRight ⊆ v.toRight :=
  fun h _ => by simpa only [mem_toRight] using @h _

Monotonicity of Right Component Extraction in Disjoint Sum Finite Sets

Informal description

For any two finite sets $u$ and $v$ of elements of type $\alpha \oplus \beta$, if $u$ is a subset of $v$, then the right component extraction of $u$ is a subset of the right component extraction of $v$. In other words, if $u \subseteq v$, then $\text{toRight}(u) \subseteq \text{toRight}(v)$.

Finset.toLeft_monotone theorem

: Monotone (@toLeft α β)

Full source

lemma toLeft_monotone : Monotone (@toLeft α β) := fun _ _ => toLeft_subset_toLeft

Monotonicity of Left Component Extraction in Disjoint Sum Finite Sets

Informal description

The function $\text{toLeft} : \text{Finset} (\alpha \oplus \beta) \to \text{Finset} \alpha$ is monotone with respect to the subset relation. That is, for any two finite sets $u, v \subseteq \alpha \oplus \beta$, if $u \subseteq v$, then $\text{toLeft}(u) \subseteq \text{toLeft}(v)$.

Finset.toRight_monotone theorem

: Monotone (@toRight α β)

Full source

lemma toRight_monotone : Monotone (@toRight α β) := fun _ _ => toRight_subset_toRight

Monotonicity of Right Component Extraction in Disjoint Sum Finite Sets

Informal description

The function `toRight`, which extracts the right components from a finite set of elements in the disjoint union type $\alpha \oplus \beta$, is monotone. That is, for any two finite sets $u$ and $v$ of elements in $\alpha \oplus \beta$, if $u \subseteq v$, then $\text{toRight}(u) \subseteq \text{toRight}(v)$.

Finset.toLeft_disjSum_toRight theorem

: u.toLeft.disjSum u.toRight = u

Full source

lemma toLeft_disjSum_toRight : u.toLeft.disjSum u.toRight = u := by
  ext (x | x) <;> simp

Reconstruction of Disjoint Sum from Components

Informal description

For any finite set $u$ of elements in the disjoint union type $\alpha \oplus \beta$, the disjoint sum of the left components $\text{toLeft}(u)$ and the right components $\text{toRight}(u)$ equals $u$ itself. That is, $\text{toLeft}(u) \text{.disjSum } \text{toRight}(u) = u$.

Finset.card_toLeft_add_card_toRight theorem

: #u.toLeft + #u.toRight = #u

Full source

lemma card_toLeft_add_card_toRight : #u.toLeft + #u.toRight = #u := by
  rw [← card_disjSum, toLeft_disjSum_toRight]

Cardinality Additivity in Disjoint Sum Components: $|\text{toLeft}(u)| + |\text{toRight}(u)| = |u|$

Informal description

For any finite set $u$ of elements in the disjoint union type $\alpha \oplus \beta$, the sum of the cardinalities of the left components $\text{toLeft}(u)$ and the right components $\text{toRight}(u)$ equals the cardinality of $u$. That is, $|\text{toLeft}(u)| + |\text{toRight}(u)| = |u|$.

Finset.card_toLeft_le theorem

: #u.toLeft ≤ #u

Full source

lemma card_toLeft_le : #u.toLeft ≤ #u :=
  (Nat.le_add_right _ _).trans_eq card_toLeft_add_card_toRight

Cardinality Inequality for Left Components in Disjoint Sum: $|\text{toLeft}(u)| \leq |u|$

Informal description

For any finite set $u$ of elements in the disjoint union type $\alpha \oplus \beta$, the cardinality of the left components $\text{toLeft}(u)$ is less than or equal to the cardinality of $u$. That is, $|\text{toLeft}(u)| \leq |u|$.

Finset.card_toRight_le theorem

: #u.toRight ≤ #u

Full source

lemma card_toRight_le : #u.toRight ≤ #u :=
  (Nat.le_add_left _ _).trans_eq card_toLeft_add_card_toRight

Cardinality Bound for Right Components in Disjoint Sum: $|\text{toRight}(u)| \leq |u|$

Informal description

For any finite set $u$ of elements in the disjoint union type $\alpha \oplus \beta$, the cardinality of the right components $\text{toRight}(u)$ is less than or equal to the cardinality of $u$. That is, $|\text{toRight}(u)| \leq |u|$.

Finset.toLeft_disjSum theorem

: (s.disjSum t).toLeft = s

Full source

@[simp] lemma toLeft_disjSum : (s.disjSum t).toLeft = s := by ext x; simp

Left Projection of Disjoint Sum Equals Original Set

Informal description

For any finite sets $s$ over type $\alpha$ and $t$ over type $\beta$, the left projection of their disjoint sum $s \uplus t$ equals $s$. In other words, $\text{toLeft}(s \uplus t) = s$.

Finset.toRight_disjSum theorem

: (s.disjSum t).toRight = t

Full source

@[simp] lemma toRight_disjSum : (s.disjSum t).toRight = t := by ext x; simp

Right Projection of Disjoint Sum Equals Original Set

Informal description

For any finite sets $s$ over type $\alpha$ and $t$ over type $\beta$, the right projection of their disjoint sum equals $t$, i.e., $\text{toRight}(s \text{ disjSum } t) = t$.

Finset.disjSum_eq_iff theorem

: s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight

Full source

lemma disjSum_eq_iff : s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight :=
  ⟨fun h => by simp [← h], fun h => by simp [h, toLeft_disjSum_toRight]⟩

Characterization of Disjoint Sum Equality via Component Extraction

Informal description

For any finite sets $s$ over type $\alpha$, $t$ over type $\beta$, and $u$ over the disjoint union $\alpha \oplus \beta$, the disjoint sum $s \uplus t$ equals $u$ if and only if $s$ equals the left projection of $u$ and $t$ equals the right projection of $u$. In other words: $$ s \uplus t = u \leftrightarrow s = \text{toLeft}(u) \land t = \text{toRight}(u) $$

Finset.disjSum_subset theorem

: s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight

Full source

lemma disjSum_subset : s.disjSum t ⊆ us.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight := by simp [subset_iff]

Subset Characterization of Disjoint Sum via Component Extraction

Informal description

For any finite sets $s$ over $\alpha$, $t$ over $\beta$, and $u$ over $\alpha \oplus \beta$, the disjoint sum $s \mathbin{\text{disjSum}} t$ is a subset of $u$ if and only if $s$ is a subset of the left components of $u$ and $t$ is a subset of the right components of $u$. In other words: $$ s \mathbin{\text{disjSum}} t \subseteq u \leftrightarrow s \subseteq \text{toLeft}(u) \land t \subseteq \text{toRight}(u) $$

Finset.subset_disjSum theorem

: u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t

Full source

lemma subset_disjSum : u ⊆ s.disjSum tu ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t := by simp [subset_iff]

Characterization of Subsets of Disjoint Sum via Component Extraction

Informal description

For any finite set $u$ of elements in the disjoint union $\alpha \oplus \beta$, $u$ is a subset of the disjoint sum $s \mathbin{\text{disjSum}} t$ if and only if the left components of $u$ are contained in $s$ and the right components of $u$ are contained in $t$. In other words: $$ u \subseteq s \mathbin{\text{disjSum}} t \leftrightarrow \text{toLeft}(u) \subseteq s \land \text{toRight}(u) \subseteq t $$

Finset.subset_map_inl theorem

: u ⊆ s.map .inl ↔ u.toLeft ⊆ s ∧ u.toRight = ∅

Full source

lemma subset_map_inl : u ⊆ s.map .inlu ⊆ s.map .inl ↔ u.toLeft ⊆ s ∧ u.toRight = ∅ := by
  simp [← disjSum_empty, subset_disjSum]

Subset Characterization of Left Injection Image via Component Extraction

Informal description

For any finite set $u$ of elements in the disjoint union $\alpha \oplus \beta$ and any finite set $s$ of elements in $\alpha$, $u$ is a subset of the image of $s$ under the left injection map $\text{inl}$ if and only if the left components of $u$ are contained in $s$ and $u$ has no right components. In symbols: $$ u \subseteq \text{map}(\text{inl})(s) \leftrightarrow \text{toLeft}(u) \subseteq s \land \text{toRight}(u) = \emptyset $$

Finset.subset_map_inr theorem

: u ⊆ t.map .inr ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t

Full source

lemma subset_map_inr : u ⊆ t.map .inru ⊆ t.map .inr ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t := by
  simp [← empty_disjSum, subset_disjSum]

Subset Characterization for Right Injection Image: $u \subseteq \text{inr}(t) \leftrightarrow u.\text{left} = \emptyset \land u.\text{right} \subseteq t$

Informal description

For any finite set $u$ of elements in the disjoint union $\alpha \oplus \beta$, $u$ is a subset of the image of $t$ under the right injection $\text{inr}$ if and only if $u$ contains no left components (i.e., $\text{toLeft}(u) = \emptyset$) and the right components of $u$ are contained in $t$ (i.e., $\text{toRight}(u) \subseteq t$). In symbols: $$ u \subseteq \text{map}(\text{inr})(t) \leftrightarrow \text{toLeft}(u) = \emptyset \land \text{toRight}(u) \subseteq t $$

Finset.map_inl_subset_iff_subset_toLeft theorem

: s.map .inl ⊆ u ↔ s ⊆ u.toLeft

Full source

lemma map_inl_subset_iff_subset_toLeft : s.map .inl ⊆ us.map .inl ⊆ u ↔ s ⊆ u.toLeft := by
  simp [← disjSum_empty, disjSum_subset]

Subset Relation Between Left Injection Image and Left Components

Informal description

For any finite set $s$ of type $\alpha$ and any finite set $u$ of type $\alpha \oplus \beta$, the image of $s$ under the left injection map $\text{inl}$ is a subset of $u$ if and only if $s$ is a subset of the left components of $u$. In symbols: \[ \text{map}(\text{inl})(s) \subseteq u \leftrightarrow s \subseteq \text{toLeft}(u) \]

Finset.map_inr_subset_iff_subset_toRight theorem

: t.map .inr ⊆ u ↔ t ⊆ u.toRight

Full source

lemma map_inr_subset_iff_subset_toRight : t.map .inr ⊆ ut.map .inr ⊆ u ↔ t ⊆ u.toRight := by
  simp [← empty_disjSum, disjSum_subset]

Right Injection Image Subset Condition: $\text{inr}(t) \subseteq u \leftrightarrow t \subseteq u.\text{toRight}$

Informal description

For any finite set $t$ of elements of type $\beta$ and any finite set $u$ of elements of type $\alpha \oplus \beta$, the image of $t$ under the right injection $\text{inr}$ is a subset of $u$ if and only if $t$ is a subset of the right components of $u$ (i.e., $t \subseteq u.\text{toRight}$).

Finset.gc_map_inl_toLeft theorem

: GaloisConnection (·.map (.inl : α ↪ α ⊕ β)) toLeft

Full source

lemma gc_map_inl_toLeft : GaloisConnection (·.map (.inl : α ↪ α ⊕ β)) toLeft :=
  fun _ _ ↦ map_inl_subset_iff_subset_toLeft

Galois Connection Between Left Injection and Left Component Extraction

Informal description

For any type $\alpha$ and $\beta$, the pair of functions $(s \mapsto \text{map}(\text{inl}, s), \text{toLeft})$ forms a Galois connection between the partial orders of finite subsets of $\alpha$ and finite subsets of $\alpha \oplus \beta$. Here: - $\text{map}(\text{inl}, s)$ is the image of finite set $s \subseteq \alpha$ under the left injection into $\alpha \oplus \beta$ - $\text{toLeft}(u)$ extracts all left components from a finite set $u \subseteq \alpha \oplus \beta$ The Galois connection means that for any $s \in \text{Finset}(\alpha)$ and $u \in \text{Finset}(\alpha \oplus \beta)$: \[ \text{map}(\text{inl}, s) \subseteq u \iff s \subseteq \text{toLeft}(u) \]

Finset.gc_map_inr_toRight theorem

: GaloisConnection (·.map (.inr : β ↪ α ⊕ β)) toRight

Full source

lemma gc_map_inr_toRight : GaloisConnection (·.map (.inr : β ↪ α ⊕ β)) toRight :=
  fun _ _ ↦ map_inr_subset_iff_subset_toRight

Galois Connection Between Right Injection and Right Extraction in Disjoint Sum Finite Sets

Informal description

For any type $\alpha$ and $\beta$, the pair of functions consisting of the right injection mapping $\text{map}(\text{inr}) : \text{Finset} \beta \to \text{Finset} (\alpha \oplus \beta)$ and the right component extraction $\text{toRight} : \text{Finset} (\alpha \oplus \beta) \to \text{Finset} \beta$ forms a Galois connection. In other words, for any finite set $t \subseteq \beta$ and any finite set $u \subseteq \alpha \oplus \beta$, we have: \[ \text{map}(\text{inr}, t) \subseteq u \quad \text{if and only if} \quad t \subseteq \text{toRight}(u). \]

Finset.toLeft_map_sumComm theorem

: (u.map (Equiv.sumComm _ _).toEmbedding).toLeft = u.toRight

Full source

@[simp] lemma toLeft_map_sumComm : (u.map (Equiv.sumComm _ _).toEmbedding).toLeft = u.toRight := by
  ext x; simp

Left Extraction of Mapped Commutative Sum Equals Right Extraction

Informal description

For any finite set $u$ of elements of type $\alpha \oplus \beta$, the left component extraction of the image of $u$ under the sum type commutativity equivalence equals the right component extraction of $u$. In other words, $\text{toLeft}(\text{map}(\text{sumComm}_{\alpha,\beta}, u)) = \text{toRight}(u)$.

Finset.toRight_map_sumComm theorem

: (u.map (Equiv.sumComm _ _).toEmbedding).toRight = u.toLeft

Full source

@[simp] lemma toRight_map_sumComm : (u.map (Equiv.sumComm _ _).toEmbedding).toRight = u.toLeft := by
  ext x; simp

Right Projection of Commuted Sum Equals Left Projection

Informal description

For any finite set $u$ of elements in the disjoint sum type $\alpha \oplus \beta$, the right projection of the image of $u$ under the sum commutativity equivalence $\alpha \oplus \beta \simeq \beta \oplus \alpha$ is equal to the left projection of $u$. In symbols, $\text{toRight}(\text{map}(\text{sumComm}_{\alpha,\beta}, u)) = \text{toLeft}(u)$.

Finset.toLeft_cons_inl theorem

(ha) : (cons (inl a) u ha).toLeft = cons a u.toLeft (by simpa)

Full source

@[simp] lemma toLeft_cons_inl (ha) :
    (cons (inl a) u ha).toLeft = cons a u.toLeft (by simpa) := by ext y; simp

Left Projection Preserves Disjoint Union with Left Injection

Informal description

Given a finite set $u$ of elements of type $\alpha \oplus \beta$, an element $a \in \alpha$, and a proof $ha$ that $\text{inl}(a) \notin u$, the left projection of the set $\text{cons}(\text{inl}(a), u, ha)$ is equal to $\text{cons}(a, \text{toLeft}(u), h')$, where $h'$ is a proof that $a \notin \text{toLeft}(u)$ (which follows from $ha$).

Finset.toLeft_cons_inr theorem

(hb) : (cons (inr b) u hb).toLeft = u.toLeft

Full source

@[simp] lemma toLeft_cons_inr (hb) :
    (cons (inr b) u hb).toLeft = u.toLeft := by ext y; simp

Left Projection Invariance Under Right-Summed Element Addition

Informal description

For any finite set $u$ of elements of type $\alpha \oplus \beta$, and any element $b \in \beta$ with proof $hb$ that $\text{inr } b \notin u$, the left projection of the set $\{\text{inr } b\} \cup u$ equals the left projection of $u$. In other words, adding a right-summed element to $u$ does not affect its left projection.

Finset.toRight_cons_inl theorem

(ha) : (cons (inl a) u ha).toRight = u.toRight

Full source

@[simp] lemma toRight_cons_inl (ha) :
    (cons (inl a) u ha).toRight = u.toRight := by ext y; simp

Right Component Extraction is Unaffected by Left-Summed Element Addition

Informal description

For any finite set $u$ of elements in the disjoint sum type $\alpha \oplus \beta$, and any element $a \in \alpha$ with proof $ha$ that $\text{inl}(a) \notin u$, the right component extraction of the set $\text{cons}(\text{inl}(a), u, ha)$ is equal to the right component extraction of $u$. In other words, adding a left-summed element to $u$ does not affect its right component extraction.

Finset.toRight_cons_inr theorem

(hb) : (cons (inr b) u hb).toRight = cons b u.toRight (by simpa)

Full source

@[simp] lemma toRight_cons_inr (hb) :
    (cons (inr b) u hb).toRight = cons b u.toRight (by simpa) := by ext y; simp

Right Projection Preserves Union with Singleton in Disjoint Sum

Informal description

For any finite set $u$ of elements in the disjoint sum type $\alpha \oplus \beta$, and any element $b \in \beta$ such that $\text{inr } b \notin u$, the right projection of the set $\{\text{inr } b\} \cup u$ is equal to $\{b\} \cup \text{toRight}(u)$, where $\text{toRight}(u)$ is the set of all right components of $u$. In symbols: $$\text{toRight}(\{\text{inr } b\} \cup u) = \{b\} \cup \text{toRight}(u)$$

Finset.toLeft_image_swap theorem

: (u.image Sum.swap).toLeft = u.toRight

Full source

lemma toLeft_image_swap : (u.image Sum.swap).toLeft = u.toRight := by
  ext x; simp

Left Projection of Swapped Disjoint Sum Equals Right Projection

Informal description

For any finite set $u$ of elements in the disjoint sum type $\alpha \oplus \beta$, the left projection of the image of $u$ under the swap function (which exchanges $\alpha$ and $\beta$) is equal to the right projection of $u$. In other words, $\text{toLeft}(\text{image}(\text{swap}, u)) = \text{toRight}(u)$.

Finset.toRight_image_swap theorem

: (u.image Sum.swap).toRight = u.toLeft

Full source

lemma toRight_image_swap : (u.image Sum.swap).toRight = u.toLeft := by
  ext x; simp

Equality of Right Extraction of Swapped Image and Left Extraction

Informal description

For any finite set $u$ of elements of type $\alpha \oplus \beta$, the right component extraction of the image of $u$ under the swap function (which exchanges $\alpha$ and $\beta$) is equal to the left component extraction of $u$. In symbols: $$\text{toRight}(\text{image}(\text{swap}, u)) = \text{toLeft}(u)$$

Finset.toLeft_insert_inl theorem

: (insert (inl a) u).toLeft = insert a u.toLeft

Full source

@[simp] lemma toLeft_insert_inl : (insert (inl a) u).toLeft = insert a u.toLeft := by ext y; simp

Left Projection Commutes with Insertion of Left Element

Informal description

For any finite set $u$ of elements in the disjoint sum type $\alpha \oplus \beta$ and any element $a \in \alpha$, the left projection of the set obtained by inserting $\text{inl } a$ into $u$ is equal to the set obtained by inserting $a$ into the left projection of $u$. In symbols: \[ \text{toLeft}(\{\text{inl } a\} \cup u) = \{a\} \cup \text{toLeft}(u) \]

Finset.toLeft_insert_inr theorem

: (insert (inr b) u).toLeft = u.toLeft

Full source

@[simp] lemma toLeft_insert_inr : (insert (inr b) u).toLeft = u.toLeft := by ext y; simp

Left Projection Preserved Under Right Insertion in Disjoint Sum Finite Sets

Informal description

For any finite set $u$ of elements of type $\alpha \oplus \beta$ and any element $b \in \beta$, the left projection of the set obtained by inserting $\text{inr } b$ into $u$ is equal to the left projection of $u$. In other words, $\text{toLeft}(\{\text{inr } b\} \cup u) = \text{toLeft}(u)$.

Finset.toRight_insert_inl theorem

: (insert (inl a) u).toRight = u.toRight

Full source

@[simp] lemma toRight_insert_inl : (insert (inl a) u).toRight = u.toRight := by ext y; simp

Right Component Preservation under Left Insertion in Disjoint Sum Finite Sets

Informal description

For any finite set $u$ of elements of type $\alpha \oplus \beta$ and any element $a \in \alpha$, inserting $\text{inl}(a)$ into $u$ does not change the right component of $u$, i.e., $\text{toRight}(\text{insert}(\text{inl}(a), u)) = \text{toRight}(u)$.

Finset.toRight_insert_inr theorem

: (insert (inr b) u).toRight = insert b u.toRight

Full source

@[simp] lemma toRight_insert_inr : (insert (inr b) u).toRight = insert b u.toRight := by ext y; simp

Right Component Extraction Preserves Insertion of Right Elements

Informal description

For any finite set $u$ of elements in the disjoint sum type $\alpha \oplus \beta$ and any element $b \in \beta$, the right component extraction of the set obtained by inserting $\text{inr } b$ into $u$ is equal to the set obtained by inserting $b$ into the right component extraction of $u$. In other words, $\text{toRight}(\{\text{inr } b\} \cup u) = \{b\} \cup \text{toRight}(u)$.

Finset.toLeft_inter theorem

: (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Full source

lemma toLeft_inter : (u ∩ v).toLeft = u.toLeft ∩ v.toLeft := by ext x; simp

Left Projection Preserves Intersection of Disjoint Sum Finite Sets

Informal description

For any two finite sets $u$ and $v$ of elements of type $\alpha \oplus \beta$, the left projection of their intersection equals the intersection of their left projections. That is, $\text{toLeft}(u \cap v) = \text{toLeft}(u) \cap \text{toLeft}(v)$.

Finset.toRight_inter theorem

: (u ∩ v).toRight = u.toRight ∩ v.toRight

Full source

lemma toRight_inter : (u ∩ v).toRight = u.toRight ∩ v.toRight := by ext x; simp

Right Projection Preserves Intersection in Disjoint Sum Finite Sets

Informal description

For any two finite sets $u$ and $v$ of elements of type $\alpha \oplus \beta$, the right projection of their intersection equals the intersection of their right projections. In symbols: \[ \text{toRight}(u \cap v) = \text{toRight}(u) \cap \text{toRight}(v) \] where $\text{toRight}(u)$ denotes the finite set $\{b : \beta \mid \text{inr } b \in u\}$.

Finset.toLeft_union theorem

: (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Full source

lemma toLeft_union : (u ∪ v).toLeft = u.toLeft ∪ v.toLeft := by ext x; simp

Left Projection Preserves Union in Disjoint Sum Finite Sets

Informal description

For any two finite sets $u$ and $v$ of elements in the disjoint sum type $\alpha \oplus \beta$, the left projection of their union equals the union of their left projections. That is, $\text{toLeft}(u \cup v) = \text{toLeft}(u) \cup \text{toLeft}(v)$.

Finset.toRight_union theorem

: (u ∪ v).toRight = u.toRight ∪ v.toRight

Full source

lemma toRight_union : (u ∪ v).toRight = u.toRight ∪ v.toRight := by ext x; simp

Right Projection Preserves Union in Disjoint Sum Finite Sets

Informal description

For any two finite sets $u$ and $v$ of elements of type $\alpha \oplus \beta$, the right projection of their union equals the union of their right projections. That is, $\text{toRight}(u \cup v) = \text{toRight}(u) \cup \text{toRight}(v)$.

Finset.toLeft_sdiff theorem

: (u \ v).toLeft = u.toLeft \ v.toLeft

Full source

lemma toLeft_sdiff : (u \ v).toLeft = u.toLeft \ v.toLeft := by ext x; simp

Set Difference Commutes with Left Component Extraction in Disjoint Sum Finite Sets

Informal description

For any finite sets $u$ and $v$ of type $\alpha \oplus \beta$, the left component extraction of the set difference $u \setminus v$ is equal to the set difference of the left component extractions of $u$ and $v$, i.e., \[ \text{toLeft}(u \setminus v) = \text{toLeft}(u) \setminus \text{toLeft}(v). \]

Finset.toRight_sdiff theorem

: (u \ v).toRight = u.toRight \ v.toRight

Full source

lemma toRight_sdiff : (u \ v).toRight = u.toRight \ v.toRight := by ext x; simp

Right Component Extraction Preserves Set Difference

Informal description

For any two finite sets $u$ and $v$ of elements of type $\alpha \oplus \beta$, the right component extraction of their set difference equals the set difference of their right component extractions, i.e., \[ \text{toRight}(u \setminus v) = \text{toRight}(u) \setminus \text{toRight}(v). \]

Finset.sumEquiv definition

{α β : Type*} : Finset (α ⊕ β) ≃o Finset α × Finset β

Full source

/-- Finsets on sum types are equivalent to pairs of finsets on each summand. -/
@[simps apply_fst apply_snd]
def sumEquiv {α β : Type*} : FinsetFinset (α ⊕ β) ≃o Finset α × Finset β where
  toFun s := (s.toLeft, s.toRight)
  invFun s := disjSum s.1 s.2
  left_inv s := toLeft_disjSum_toRight
  right_inv s := by simp
  map_rel_iff' := by simp [← Finset.coe_subset, Set.subset_def]

Order isomorphism between finite sets of a disjoint union and product of finite sets

Informal description

The order isomorphism $\text{Finset}(\alpha \oplus \beta) \simeq_o \text{Finset}(\alpha) \times \text{Finset}(\beta)$ between the finite sets of a disjoint union type $\alpha \oplus \beta$ and the product of finite sets over $\alpha$ and $\beta$. The forward direction maps a finite set $s$ of $\alpha \oplus \beta$ to the pair $(\text{toLeft}(s), \text{toRight}(s))$ consisting of its left and right components. The inverse direction maps a pair $(s, t)$ to the disjoint sum $\text{disjSum}(s, t)$. This isomorphism preserves the order structure, meaning $s \subseteq s'$ if and only if $\text{toLeft}(s) \subseteq \text{toLeft}(s')$ and $\text{toRight}(s) \subseteq \text{toRight}(s')$.

Finset.sumEquiv_symm_apply theorem

{α β : Type*} (s : Finset α × Finset β) : sumEquiv.symm s = disjSum s.1 s.2

Full source

@[simp]
lemma sumEquiv_symm_apply {α β : Type*} (s : FinsetFinset α × Finset β) :
    sumEquiv.symm s = disjSum s.1 s.2 := rfl

Inverse of Sum Equivalence Maps to Disjoint Sum

Informal description

For any pair of finite sets $(s, t)$ where $s$ is a finite subset of $\alpha$ and $t$ is a finite subset of $\beta$, the inverse of the order isomorphism $\text{sumEquiv}$ maps $(s, t)$ to the disjoint sum $\text{disjSum}(s, t)$ of $s$ and $t$ in the finite set of the disjoint union type $\alpha \oplus \beta$.

Finset.map_disjSum theorem

 (f : α ⊕ β ↪ γ) :
  (s.disjSum t).map f =
    (s.map (.trans .inl f)).disjUnion (t.map (.trans .inr f))
      (by as_aux_lemma => simpa only [← map_map] using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _))

Full source

theorem map_disjSum (f : α ⊕ βα ⊕ β ↪ γ) :
    (s.disjSum t).map f =
      (s.map (.trans .inl f)).disjUnion (t.map (.trans .inr f)) (by
        as_aux_lemma =>
          simpa only [← map_map]
            using (Finset.disjoint_map f).2 (disjoint_map_inl_map_inr _ _)) :=
  val_injective <| Multiset.map_disjSum _

Image of Disjoint Sum under Embedding Equals Disjoint Union of Component Images

Informal description

Given an injective function embedding $f : \alpha \oplus \beta \hookrightarrow \gamma$ and finite sets $s$ over $\alpha$ and $t$ over $\beta$, the image of the disjoint sum $s.\text{disjSum}\, t$ under $f$ is equal to the disjoint union of: 1. The image of $s$ under the composition of the left injection $\text{inl} : \alpha \hookrightarrow \alpha \oplus \beta$ with $f$ 2. The image of $t$ under the composition of the right injection $\text{inr} : \beta \hookrightarrow \alpha \oplus \beta$ with $f$ Moreover, these two images are disjoint. In symbols: $$ \text{map}\, f\, (s.\text{disjSum}\, t) = \text{map}\, (f \circ \text{inl})\, s \sqcup \text{map}\, (f \circ \text{inr})\, t $$ where $\sqcup$ denotes disjoint union.

Finset.fold_disjSum theorem

 (s : Finset α) (t : Finset β) (f : α ⊕ β → γ) (b₁ b₂ : γ) (op : γ → γ → γ) [Std.Commutative op] [Std.Associative op] :
  (s.disjSum t).fold op (op b₁ b₂) f = op (s.fold op b₁ (f <| .inl ·)) (t.fold op b₂ (f <| .inr ·))

Full source

lemma fold_disjSum (s : Finset α) (t : Finset β) (f : α ⊕ β → γ) (b₁ b₂ : γ) (op : γ → γ → γ)
    [Std.Commutative op] [Std.Associative op] :
    (s.disjSum t).fold op (op b₁ b₂) f =
      op (s.fold op b₁ (f <| .inl ·)) (t.fold op b₂ (f <| .inr ·)) := by
  simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]

Additivity of Fold over Disjoint Sum of Finite Sets

Informal description

Let $s$ be a finite set over $\alpha$, $t$ a finite set over $\beta$, $f : \alpha \oplus \beta \to \gamma$ a function, and $b_1, b_2 \in \gamma$ elements. Given a commutative and associative binary operation $op : \gamma \to \gamma \to \gamma$, the fold of the disjoint sum $s.disjSum\, t$ with initial value $op\, b_1\, b_2$ under $f$ equals the $op$-combination of: 1. The fold of $s$ with initial value $b_1$ under $f \circ \text{inl}$ 2. The fold of $t$ with initial value $b_2$ under $f \circ \text{inr}$ That is: $$ (s.disjSum\, t).\text{fold}\, op\, (op\, b_1\, b_2)\, f = op\, (s.\text{fold}\, op\, b_1\, (f \circ \text{inl}))\, (t.\text{fold}\, op\, b_2\, (f \circ \text{inr})) $$

Main declarations