Mathlib.Data.Multiset.Replicate

Multiset.replicate definition

(n : ℕ) (a : α) : Multiset α

Full source

/-- `replicate n a` is the multiset containing only `a` with multiplicity `n`. -/
def replicate (n : ℕ) (a : α) : Multiset α :=
  List.replicate n a

Multiset with repeated element

Informal description

The function `replicate n a` constructs the multiset containing the element $a$ with multiplicity $n$. When $n = 0$, this gives the empty multiset.

Multiset.coe_replicate theorem

(n : ℕ) (a : α) : (List.replicate n a : Multiset α) = replicate n a

Full source

theorem coe_replicate (n : ℕ) (a : α) : (List.replicate n a : Multiset α) = replicate n a := rfl

Equality of Coerced Replicated List and Replicated Multiset

Informal description

For any natural number $n$ and any element $a$ of type $\alpha$, the multiset obtained by coercing the list `List.replicate n a` (which contains $n$ copies of $a$) is equal to the multiset `replicate n a` (the multiset containing $a$ with multiplicity $n$).

Multiset.replicate_zero theorem

(a : α) : replicate 0 a = 0

Full source

@[simp] theorem replicate_zero (a : α) : replicate 0 a = 0 := rfl

Empty Replicated Multiset: $\text{replicate}(0, a) = 0$

Informal description

For any element $a$ of type $\alpha$, the multiset obtained by replicating $a$ zero times is equal to the empty multiset, i.e., $\text{replicate}(0, a) = 0$.

Multiset.replicate_succ theorem

(a : α) (n) : replicate (n + 1) a = a ::ₘ replicate n a

Full source

@[simp] theorem replicate_succ (a : α) (n) : replicate (n + 1) a = a ::ₘ replicate n a := rfl

Recursive Construction of Replicated Multisets: $\text{replicate}(n+1, a) = a \text{ ::ₘ } \text{replicate}(n, a)$

Informal description

For any element $a$ of type $\alpha$ and any natural number $n$, the multiset obtained by replicating $a$ exactly $n+1$ times is equal to the multiset formed by adding one occurrence of $a$ to the multiset obtained by replicating $a$ $n$ times. In symbols: $$\text{replicate}(n+1, a) = a \text{ ::ₘ } \text{replicate}(n, a)$$

Multiset.replicate_add theorem

(m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a

Full source

theorem replicate_add (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a :=
  congr_arg _ <| List.replicate_add ..

Additivity of Multiset Replication: $\text{replicate}(m + n, a) = \text{replicate}(m, a) + \text{replicate}(n, a)$

Informal description

For any natural numbers $m$ and $n$ and any element $a$ of type $\alpha$, the multiset obtained by replicating $a$ exactly $m + n$ times is equal to the sum of the multiset with $a$ replicated $m$ times and the multiset with $a$ replicated $n$ times. In other words: $$\text{replicate}(m + n, a) = \text{replicate}(m, a) + \text{replicate}(n, a)$$

Multiset.replicate_one theorem

(a : α) : replicate 1 a = { a }

Full source

theorem replicate_one (a : α) : replicate 1 a = {a} := rfl

Replicating Once Yields Singleton Multiset: $\text{replicate}(1, a) = \{a\}$

Informal description

For any element $a$ of type $\alpha$, the multiset obtained by replicating $a$ exactly once is equal to the singleton multiset containing $a$, i.e., $\text{replicate}(1, a) = \{a\}$.

Multiset.card_replicate theorem

(n) (a : α) : card (replicate n a) = n

Full source

@[simp] theorem card_replicate (n) (a : α) : card (replicate n a) = n :=
  length_replicate

Cardinality of Replicated Multiset: $|\text{replicate}(n, a)| = n$

Informal description

For any natural number $n$ and any element $a$ of type $\alpha$, the cardinality of the multiset $\text{replicate}(n, a)$ is equal to $n$.

Multiset.mem_replicate theorem

{a b : α} {n : ℕ} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

Full source

theorem mem_replicate {a b : α} {n : ℕ} : b ∈ replicate n ab ∈ replicate n a ↔ n ≠ 0 ∧ b = a :=
  List.mem_replicate

Membership in Replicated Multiset: $b \in \text{replicate}(n, a) \leftrightarrow n \neq 0 \land b = a$

Informal description

For any elements $a, b$ in a type $\alpha$ and any natural number $n$, the element $b$ belongs to the multiset $\text{replicate}(n, a)$ if and only if $n \neq 0$ and $b = a$.

Multiset.replicate_right_injective theorem

{n : ℕ} (hn : n ≠ 0) : Injective (@replicate α n)

Full source

theorem replicate_right_injective {n : ℕ} (hn : n ≠ 0) : Injective (@replicate α n) :=
  fun _ _ h => (eq_replicate.1 h).2 _ <| mem_replicate.2 ⟨hn, rfl⟩

Injectivity of Multiset Replication for Nonzero Counts

Informal description

For any nonzero natural number $n$, the function that maps an element $a$ to the multiset $\text{replicate}(n, a)$ (containing $a$ with multiplicity $n$) is injective. That is, for any elements $a$ and $b$ of type $\alpha$, if $\text{replicate}(n, a) = \text{replicate}(n, b)$, then $a = b$.

Multiset.replicate_right_inj theorem

{a b : α} {n : ℕ} (h : n ≠ 0) : replicate n a = replicate n b ↔ a = b

Full source

@[simp] theorem replicate_right_inj {a b : α} {n : ℕ} (h : n ≠ 0) :
    replicatereplicate n a = replicate n b ↔ a = b :=
  (replicate_right_injective h).eq_iff

Equality of Replicated Multisets Implies Element Equality for Nonzero Counts

Informal description

For any elements $a$ and $b$ of type $\alpha$ and any nonzero natural number $n$, the multiset $\text{replicate}(n, a)$ is equal to $\text{replicate}(n, b)$ if and only if $a = b$.

Multiset.replicate_left_injective theorem

(a : α) : Injective (replicate · a)

Full source

theorem replicate_left_injective (a : α) : Injective (replicate · a) :=
  LeftInverse.injective (card_replicate · a)

Injectivity of Replication Count in Multisets: $n \mapsto \text{replicate}(n, a)$

Informal description

For any element $a$ of type $\alpha$, the function $n \mapsto \text{replicate}(n, a)$ (which constructs a multiset containing $a$ with multiplicity $n$) is injective. That is, for any natural numbers $n$ and $m$, if $\text{replicate}(n, a) = \text{replicate}(m, a)$, then $n = m$.

Multiset.replicate_subset_singleton theorem

(n : ℕ) (a : α) : replicate n a ⊆ { a }

Full source

theorem replicate_subset_singleton (n : ℕ) (a : α) : replicatereplicate n a ⊆ {a} :=
  List.replicate_subset_singleton n a

Replicated Multiset is Subset of Singleton: $\text{replicate}(n, a) \subseteq \{a\}$

Informal description

For any natural number $n$ and any element $a$ of type $\alpha$, the multiset $\text{replicate}(n, a)$ (containing $a$ with multiplicity $n$) is a subset of the singleton multiset $\{a\}$.

Multiset.replicate_le_coe theorem

{a : α} {n} {l : List α} : replicate n a ≤ l ↔ List.replicate n a <+ l

Full source

theorem replicate_le_coe {a : α} {n} {l : List α} : replicatereplicate n a ≤ l ↔ List.replicate n a <+ l :=
  ⟨fun ⟨_l', p, s⟩ => perm_replicate.1 p ▸ s, Sublist.subperm⟩

Sub-multiset Condition for Replicated Multisets via Sublists

Informal description

For any element $a$ of type $\alpha$, natural number $n$, and list $l$ of type $\alpha$, the multiset $\text{replicate}(n, a)$ is a sub-multiset of the multiset constructed from $l$ if and only if the list $\text{List.replicate}(n, a)$ is a sublist of $l$.

Multiset.replicate_le_replicate theorem

(a : α) {k n : ℕ} : replicate k a ≤ replicate n a ↔ k ≤ n

Full source

theorem replicate_le_replicate (a : α) {k n : ℕ} : replicatereplicate k a ≤ replicate n a ↔ k ≤ n :=
  _root_.trans (by rw [← replicate_le_coe, coe_replicate]) (List.replicate_sublist_replicate a)

Sub-multiset Condition for Replicated Multisets: $\text{replicate}(k, a) \leq \text{replicate}(n, a) \leftrightarrow k \leq n$

Informal description

For any element $a$ of type $\alpha$ and natural numbers $k, n$, the multiset $\text{replicate}(k, a)$ (containing $a$ with multiplicity $k$) is a sub-multiset of $\text{replicate}(n, a)$ if and only if $k \leq n$.

Multiset.replicate_mono theorem

(a : α) {k n : ℕ} (h : k ≤ n) : replicate k a ≤ replicate n a

Full source

@[gcongr]
theorem replicate_mono (a : α) {k n : ℕ} (h : k ≤ n) : replicate k a ≤ replicate n a :=
  (replicate_le_replicate a).2 h

Monotonicity of Replicated Multisets: $\text{replicate}(k, a) \leq \text{replicate}(n, a)$ when $k \leq n$

Informal description

For any element $a$ of type $\alpha$ and natural numbers $k, n$ such that $k \leq n$, the multiset $\text{replicate}(k, a)$ (containing $a$ with multiplicity $k$) is a sub-multiset of $\text{replicate}(n, a)$ (containing $a$ with multiplicity $n$).

Multiset.le_replicate_iff theorem

{m : Multiset α} {a : α} {n : ℕ} : m ≤ replicate n a ↔ ∃ k ≤ n, m = replicate k a

Full source

theorem le_replicate_iff {m : Multiset α} {a : α} {n : ℕ} :
    m ≤ replicate n a ↔ ∃ k ≤ n, m = replicate k a :=
  ⟨fun h => ⟨card m, (card_mono h).trans_eq (card_replicate _ _),
      eq_replicate_card.2 fun _ hb => eq_of_mem_replicate <| subset_of_le h hb⟩,
    fun ⟨_, hkn, hm⟩ => hm.symm ▸ (replicate_le_replicate _).2 hkn⟩

Sub-multiset Characterization for Replicated Multisets: $m \leq \text{replicate}(n, a) \leftrightarrow \exists k \leq n, m = \text{replicate}(k, a)$

Informal description

For any multiset $m$ over a type $\alpha$, any element $a \in \alpha$, and any natural number $n$, the multiset $m$ is a sub-multiset of $\text{replicate}(n, a)$ (the multiset containing $a$ with multiplicity $n$) if and only if there exists a natural number $k \leq n$ such that $m = \text{replicate}(k, a)$.

Multiset.lt_replicate_succ theorem

{m : Multiset α} {x : α} {n : ℕ} : m < replicate (n + 1) x ↔ m ≤ replicate n x

Full source

theorem lt_replicate_succ {m : Multiset α} {x : α} {n : ℕ} :
    m < replicate (n + 1) x ↔ m ≤ replicate n x := by
  rw [lt_iff_cons_le]
  constructor
  · rintro ⟨x', hx'⟩
    have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
    rwa [this, replicate_succ, cons_le_cons_iff] at hx'
  · intro h
    rw [replicate_succ]
    exact ⟨x, cons_le_cons _ h⟩

Strict Submultiset Characterization for Replicated Multisets: $m < \text{replicate}(n+1, x) \leftrightarrow m \leq \text{replicate}(n, x)$

Informal description

For any multiset $m$ over a type $\alpha$, any element $x \in \alpha$, and any natural number $n$, the multiset $m$ is strictly contained in the multiset $\text{replicate}(n+1, x)$ (containing $x$ with multiplicity $n+1$) if and only if $m$ is a sub-multiset of $\text{replicate}(n, x)$ (containing $x$ with multiplicity $n$). In symbols: $$m < \text{replicate}(n+1, x) \leftrightarrow m \leq \text{replicate}(n, x)$$

Multiset.count_replicate_self theorem

(a : α) (n : ℕ) : count a (replicate n a) = n

Full source

@[simp]
theorem count_replicate_self (a : α) (n : ℕ) : count a (replicate n a) = n := by
  convert List.count_replicate_self (a := a)
  rw [← coe_count, coe_replicate]

Multiplicity of Element in Its Own Replicated Multiset: $\text{count } a (\text{replicate } n a) = n$

Informal description

For any element $a$ of type $\alpha$ and any natural number $n$, the multiplicity of $a$ in the multiset $\text{replicate } n a$ (the multiset containing $n$ copies of $a$) is equal to $n$. That is, $\text{count } a (\text{replicate } n a) = n$.

Multiset.count_replicate theorem

(a b : α) (n : ℕ) : count a (replicate n b) = if b = a then n else 0

Full source

theorem count_replicate (a b : α) (n : ℕ) : count a (replicate n b) = if b = a then n else 0 := by
  convert List.count_replicate (a := a)
  · rw [← coe_count, coe_replicate]
  · simp

Multiplicity in Replicated Multiset: $\text{count } a (\text{replicate } n b) = \text{if } b = a \text{ then } n \text{ else } 0$

Informal description

For any elements $a, b$ of type $\alpha$ and any natural number $n$, the multiplicity of $a$ in the multiset $\text{replicate } n b$ (the multiset containing $b$ with multiplicity $n$) is equal to $n$ if $b = a$, and $0$ otherwise. In other words: $$\text{count } a (\text{replicate } n b) = \begin{cases} n & \text{if } b = a \\ 0 & \text{otherwise} \end{cases}$$

Multiset.le_count_iff_replicate_le theorem

{a : α} {s : Multiset α} {n : ℕ} : n ≤ count a s ↔ replicate n a ≤ s

Full source

theorem le_count_iff_replicate_le {a : α} {s : Multiset α} {n : ℕ} :
    n ≤ count a s ↔ replicate n a ≤ s :=
  Quot.inductionOn s fun _l => by
    simp only [quot_mk_to_coe'', mem_coe, coe_count]
    exact le_count_iff_replicate_sublist.trans replicate_le_coe.symm

Sub-multiset Criterion via Count and Replicate: $n \leq \text{count } a s \leftrightarrow \text{replicate } n a \leq s$

Informal description

For any element $a$ of type $\alpha$, multiset $s$ over $\alpha$, and natural number $n$, the inequality $n \leq \text{count } a s$ holds if and only if the multiset $\text{replicate } n a$ is a sub-multiset of $s$.

Multiset.rel_replicate_left theorem

 {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} : (replicate n a).Rel r m ↔ card m = n ∧ ∀ x, x ∈ m → r a x

Full source

theorem rel_replicate_left {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
    (replicate n a).Rel r m ↔ card m = n ∧ ∀ x, x ∈ m → r a x :=
  ⟨fun h =>
    ⟨(card_eq_card_of_rel h).symm.trans (card_replicate _ _), fun x hx => by
      obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
      rwa [eq_of_mem_replicate hb1] at hb2⟩,
    fun h =>
    rel_of_forall (fun _ _ hx hy => (eq_of_mem_replicate hx).symm ▸ h.2 _ hy)
      (Eq.trans (card_replicate _ _) h.1.symm)⟩

Characterization of Relation Between Replicated Multiset and Another Multiset: $\text{Rel}\,r\,(\text{replicate}\,n\,a)\,m \leftrightarrow |m| = n \land \forall x \in m, r\,a\,x$

Informal description

For any multiset $m$ over a type $\alpha$, element $a \in \alpha$, relation $r : \alpha \to \alpha \to \text{Prop}$, and natural number $n$, the relation $\text{Rel}\,r\,(\text{replicate}\,n\,a)\,m$ holds if and only if the cardinality of $m$ is $n$ and for every element $x \in m$, the relation $r\,a\,x$ holds.

Multiset.rel_replicate_right theorem

 {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} : m.Rel r (replicate n a) ↔ card m = n ∧ ∀ x, x ∈ m → r x a

Full source

theorem rel_replicate_right {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
    m.Rel r (replicate n a) ↔ card m = n ∧ ∀ x, x ∈ m → r x a :=
  rel_flip.trans rel_replicate_left

Characterization of Relation Between Multiset and Replicated Multiset: $\text{Rel}\,r\,m\,(\text{replicate}\,n\,a) \leftrightarrow |m| = n \land \forall x \in m, r\,x\,a$

Informal description

For any multiset $m$ over a type $\alpha$, element $a \in \alpha$, relation $r : \alpha \to \alpha \to \text{Prop}$, and natural number $n$, the relation $\text{Rel}\,r\,m\,(\text{replicate}\,n\,a)$ holds if and only if the cardinality of $m$ is $n$ and for every element $x \in m$, the relation $r\,x\,a$ holds.

Multiset.nodup_iff_le theorem

{s : Multiset α} : Nodup s ↔ ∀ a : α, ¬a ::ₘ a ::ₘ 0 ≤ s

Full source

theorem nodup_iff_le {s : Multiset α} : NodupNodup s ↔ ∀ a : α, ¬a ::ₘ a ::ₘ 0 ≤ s :=
  Quot.induction_on s fun _ =>
    nodup_iff_sublist.trans <| forall_congr' fun a => not_congr (@replicate_le_coe _ a 2 _).symm

Characterization of Duplicate-Free Multisets via Sub-multiset Condition

Informal description

A multiset $s$ over a type $\alpha$ has no duplicate elements if and only if for every element $a \in \alpha$, the multiset containing two copies of $a$ (i.e., $a ::ₘ a ::ₘ 0$) is not a sub-multiset of $s$.

Multiset.nodup_iff_ne_cons_cons theorem

{s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a ::ₘ a ::ₘ t

Full source

theorem nodup_iff_ne_cons_cons {s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a ::ₘ a ::ₘ t :=
  nodup_iff_le.trans
    ⟨fun h a _ s_eq => h a (s_eq.symm ▸ cons_le_cons a (cons_le_cons a (zero_le _))), fun h a le =>
      let ⟨t, s_eq⟩ := le_iff_exists_add.mp le
      h a t (by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq)⟩

Characterization of Duplicate-Free Multisets via Double Insertion Inequality

Informal description

A multiset $s$ over a type $\alpha$ has no duplicate elements if and only if for every element $a \in \alpha$ and every multiset $t$ over $\alpha$, $s$ is not equal to the multiset obtained by adding two copies of $a$ to $t$ (i.e., $s \neq a \mathbin{::} a \mathbin{::} t$).

Multiset.nodup_iff_pairwise theorem

{α} {s : Multiset α} : Nodup s ↔ Pairwise (· ≠ ·) s

Full source

theorem nodup_iff_pairwise {α} {s : Multiset α} : NodupNodup s ↔ Pairwise (· ≠ ·) s :=
  Quotient.inductionOn s fun _ => (pairwise_coe_iff_pairwise fun _ _ => Ne.symm).symm

Characterization of Duplicate-Free Multisets via Pairwise Inequality

Informal description

A multiset $s$ over a type $\alpha$ has no duplicate elements if and only if the relation $\neq$ holds pairwise for all distinct elements in $s$. In other words, $s$ is `Nodup` precisely when there exists a list representation of $s$ where all distinct elements are pairwise unequal.

Multiset.Nodup.pairwise theorem

: (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) → Nodup s → Pairwise r s

Full source

protected theorem Nodup.pairwise : (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) → Nodup s → Pairwise r s :=
  Quotient.inductionOn s fun l h hl => ⟨l, rfl, hl.imp_of_mem fun {a b} ha hb => h a ha b hb⟩

Pairwise Relation Holds on Distinct Elements of a Nodup Multiset

Informal description

For any multiset $s$ over a type $\alpha$ and any binary relation $r$ on $\alpha$, if for all distinct elements $a, b \in s$ the relation $r(a, b)$ holds, and $s$ has no duplicate elements (i.e., $s$ is `Nodup`), then the multiset $s$ satisfies the pairwise relation `Pairwise r s$.

Main definitions