Mathlib.Data.Multiset.Sum

Multiset.disjSum definition

: Multiset (α ⊕ β)

Full source

/-- Disjoint sum of multisets. -/
def disjSum : Multiset (α ⊕ β) :=
  s.map inl + t.map inr

Disjoint sum of multisets

Informal description

The disjoint sum of two multisets $s$ over $\alpha$ and $t$ over $\beta$ is the multiset over $\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}$.

Multiset.zero_disjSum theorem

: (0 : Multiset α).disjSum t = t.map inr

Full source

@[simp]
theorem zero_disjSum : (0 : Multiset α).disjSum t = t.map inr :=
  Multiset.zero_add _

Disjoint Sum with Empty Left Multiset Yields Right Inclusion Image

Informal description

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

Multiset.disjSum_zero theorem

: s.disjSum (0 : Multiset β) = s.map inl

Full source

@[simp]
theorem disjSum_zero : s.disjSum (0 : Multiset β) = s.map inl :=
  Multiset.add_zero _

Disjoint Sum with Empty Multiset Yields Left Inclusion Image

Informal description

For any multiset $s$ over a type $\alpha$, the disjoint sum of $s$ with the empty multiset over $\beta$ is equal to the image of $s$ under the left inclusion map $\text{inl}$, i.e., $s.\text{disjSum}\, 0 = \text{inl}(s)$.

Multiset.card_disjSum theorem

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

Full source

@[simp]
theorem card_disjSum : Multiset.card (s.disjSum t) = Multiset.card s + Multiset.card t := by
  rw [disjSum, card_add, card_map, card_map]

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

Informal description

For any multisets $s$ over type $\alpha$ and $t$ over type $\beta$, the cardinality of their disjoint sum $s.disjSum t$ is equal to the sum of the cardinalities of $s$ and $t$, i.e., $|s.disjSum t| = |s| + |t|$.

Multiset.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 := by
  simp_rw [disjSum, mem_add, mem_map]

Membership in Disjoint Sum of Multisets: $x \in s \uplus t \leftrightarrow (\exists a \in s, x = \text{inl}(a)) \lor (\exists b \in t, x = \text{inr}(b))$

Informal description

An element $x$ belongs to the disjoint sum of multisets $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 other words, $x \in s.\text{disjSum}\, t \leftrightarrow (\exists a \in s, x = \text{inl}(a)) \lor (\exists b \in t, x = \text{inr}(b))$.

Multiset.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 := by
  rw [mem_disjSum, or_iff_left]
  · simp only [inl.injEq, exists_eq_right]
  rintro ⟨b, _, hb⟩
  exact inr_ne_inl hb

Membership of Left Inclusion in Disjoint Sum: $\text{inl}(a) \in s \uplus t \leftrightarrow a \in s$

Informal description

For any multiset $s$ over type $\alpha$, multiset $t$ over type $\beta$, and element $a \in \alpha$, the left inclusion $\text{inl}(a)$ is an element of the disjoint sum $s.\text{disjSum}\, t$ if and only if $a$ is an element of $s$.

Multiset.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 := by
  rw [mem_disjSum, or_iff_right]
  · simp only [inr.injEq, exists_eq_right]
  rintro ⟨a, _, ha⟩
  exact inl_ne_inr ha

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

Informal description

For any multiset $s$ over type $\alpha$, multiset $t$ over type $\beta$, and element $b \in \beta$, the right inclusion $\text{inr}(b)$ is an element of the disjoint sum $s \uplus t$ if and only if $b$ is an element of $t$.

Multiset.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₂ :=
  add_le_add (map_le_map hs) (map_le_map ht)

Monotonicity of Disjoint Sum of Multisets

Informal description

For any multisets $s₁, s₂$ over type $\alpha$ and $t₁, t₂$ over type $\beta$, if $s₁ \leq s₂$ and $t₁ \leq t₂$, then the disjoint sum $s₁.disjSum t₁$ is less than or equal to $s₂.disjSum t₂$ as multisets over $\alpha \oplus \beta$.

Multiset.disjSum_mono_left theorem

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

Full source

theorem disjSum_mono_left (t : Multiset β) : Monotone fun s : Multiset α => s.disjSum t :=
  fun _ _ hs => Multiset.add_le_add_right (map_le_map hs)

Monotonicity of Disjoint Sum in Left Argument

Informal description

For any multiset $t$ over type $\beta$, the function $s \mapsto s \uplus t$ is monotone with respect to the multiset ordering on $\alpha$ and $\alpha \oplus \beta$. That is, for any multisets $s_1, s_2$ over $\alpha$, if $s_1 \leq s_2$, then $s_1 \uplus t \leq s_2 \uplus t$.

Multiset.disjSum_mono_right theorem

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

Full source

theorem disjSum_mono_right (s : Multiset α) :
    Monotone (s.disjSum : Multiset β → Multiset (α ⊕ β)) := fun _ _ ht =>
  Multiset.add_le_add_left (map_le_map ht)

Monotonicity of Disjoint Sum in Right Argument

Informal description

For any multiset $s$ over type $\alpha$, the function $t \mapsto s \uplus t$ is monotone with respect to the multiset ordering on $\beta$ and $\alpha \oplus \beta$. That is, for any multisets $t_1, t_2$ over $\beta$, if $t_1 \leq t_2$, then $s \uplus t_1 \leq s \uplus t_2$.

Multiset.disjSum_lt_disjSum_of_lt_of_le theorem

(hs : s₁ < s₂) (ht : t₁ ≤ t₂) : s₁.disjSum t₁ < s₂.disjSum t₂

Full source

theorem disjSum_lt_disjSum_of_lt_of_le (hs : s₁ < s₂) (ht : t₁ ≤ t₂) :
    s₁.disjSum t₁ < s₂.disjSum t₂ :=
  add_lt_add_of_lt_of_le (map_lt_map hs) (map_le_map ht)

Strict Monotonicity of Disjoint Sum under Left-Strict and Right-Weak Ordering

Informal description

For any multisets $s_1, s_2$ over type $\alpha$ and $t_1, t_2$ over type $\beta$, if $s_1 < s_2$ in the multiset ordering and $t_1 \leq t_2$, then the disjoint sum $s_1 \uplus t_1$ is strictly less than the disjoint sum $s_2 \uplus t_2$ in the multiset ordering.

Multiset.disjSum_lt_disjSum_of_le_of_lt theorem

(hs : s₁ ≤ s₂) (ht : t₁ < t₂) : s₁.disjSum t₁ < s₂.disjSum t₂

Full source

theorem disjSum_lt_disjSum_of_le_of_lt (hs : s₁ ≤ s₂) (ht : t₁ < t₂) :
    s₁.disjSum t₁ < s₂.disjSum t₂ :=
  add_lt_add_of_le_of_lt (map_le_map hs) (map_lt_map ht)

Strict Monotonicity of Disjoint Sum under Partial Ordering

Informal description

For any multisets $s_1, s_2$ over type $\alpha$ and $t_1, t_2$ over type $\beta$, if $s_1 \leq s_2$ and $t_1 < t_2$, then the disjoint sum $s_1 \uplus t_1$ is strictly less than the disjoint sum $s_2 \uplus t_2$ in the multiset ordering.

Multiset.disjSum_strictMono_left theorem

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

Full source

theorem disjSum_strictMono_left (t : Multiset β) : StrictMono fun s : Multiset α => s.disjSum t :=
  fun _ _ hs => disjSum_lt_disjSum_of_lt_of_le hs le_rfl

Strict Monotonicity of Left Disjoint Sum Operation

Informal description

For any fixed multiset $t$ over type $\beta$, the function that maps a multiset $s$ over type $\alpha$ to the disjoint sum $s \uplus t$ is strictly monotone with respect to the multiset ordering. That is, if $s_1 < s_2$ in the multiset ordering, then $s_1 \uplus t < s_2 \uplus t$.

Multiset.disjSum_strictMono_right theorem

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

Full source

theorem disjSum_strictMono_right (s : Multiset α) :
    StrictMono (s.disjSum : Multiset β → Multiset (α ⊕ β)) := fun _ _ =>
  disjSum_lt_disjSum_of_le_of_lt le_rfl

Strict Monotonicity of Right Disjoint Sum Operation

Informal description

For any fixed multiset $s$ over type $\alpha$, the function that maps a multiset $t$ over type $\beta$ to the disjoint sum $s \uplus t$ is strictly monotone with respect to the multiset ordering. That is, if $t_1 < t_2$ in the multiset ordering, then $s \uplus t_1 < s \uplus t_2$.

Multiset.Nodup.disjSum theorem

(hs : s.Nodup) (ht : t.Nodup) : (s.disjSum t).Nodup

Full source

protected theorem Nodup.disjSum (hs : s.Nodup) (ht : t.Nodup) : (s.disjSum t).Nodup := by
  refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_
  rw [disjoint_map_map]
  exact fun _ _ _ _ ↦ inr_ne_inl.symm

Disjoint Sum Preserves Nodup Property

Informal description

For any multisets $s$ over $\alpha$ and $t$ over $\beta$ with no duplicate elements, their disjoint sum $s \uplus t$ (as a multiset over $\alpha \oplus \beta$) also has no duplicate elements.

Multiset.map_disjSum theorem

(f : α ⊕ β → γ) : (s.disjSum t).map f = s.map (f <| .inl ·) + t.map (f <| .inr ·)

Full source

theorem map_disjSum (f : α ⊕ β → γ) :
    (s.disjSum t).map f = s.map (f <| .inl ·) + t.map (f <| .inr ·) := by
  simp_rw [disjSum, map_add, map_map, Function.comp_def]

Image of Disjoint Sum under Function Equals Sum of Images

Informal description

For any function $f : \alpha \oplus \beta \to \gamma$ and multisets $s$ over $\alpha$ and $t$ over $\beta$, the image of the disjoint sum $s.disjSum\, t$ under $f$ is equal to the sum of the images of $s$ under $f \circ \text{inl}$ and $t$ under $f \circ \text{inr}$. In other words: $$ \text{map}\, f\, (s.disjSum\, t) = \text{map}\, (f \circ \text{inl})\, s + \text{map}\, (f \circ \text{inr})\, t $$

Main declarations