Repeating elements in multisets

Main definitions

• replicate n a is the multiset containing only a with multiplicity n

Multiset.replicate

def Multiset.replicate {α : Type u_1} (n : ℕ) (a : α) : Multiset α

replicate n a is the multiset containing only a with multiplicity n.

Equations

• Multiset.replicate n a = ↑(List.replicate n a)

theorem Multiset.coe_replicate {α : Type u_1} (n : ℕ) (a : α) : ↑(List.replicate n a) = replicate n a

@[simp]

theorem Multiset.replicate_zero {α : Type u_1} (a : α) : replicate 0 a = 0

@[simp]

theorem Multiset.replicate_succ {α : Type u_1} (a : α) (n : ℕ) : replicate (n + 1) a = a ::ₘ replicate n a

theorem Multiset.replicate_add {α : Type u_1} (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a

theorem Multiset.replicate_one {α : Type u_1} (a : α) : replicate 1 a = {a}

@[simp]

theorem Multiset.card_replicate {α : Type u_1} (n : ℕ) (a : α) : (replicate n a).card = n

theorem Multiset.mem_replicate {α : Type u_1} {a b : α} {n : ℕ} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

theorem Multiset.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : ℕ} : b ∈ replicate n a → b = a

theorem Multiset.eq_replicate_card {α : Type u_1} {a : α} {s : Multiset α} : s = replicate s.card a ↔ ∀ (b : α), b ∈ s → b = a

theorem Multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : Multiset α} : (∀ (b : α), b ∈ s → b = a) → s = replicate s.card a

Alias of the reverse direction of Multiset.eq_replicate_card.

theorem Multiset.eq_replicate {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α} : s = replicate n a ↔ s.card = n ∧ ∀ (b : α), b ∈ s → b = a

theorem Multiset.replicate_right_injective {α : Type u_1} {n : ℕ} (hn : n ≠ 0) : Function.Injective (replicate n)

@[simp]

theorem Multiset.replicate_right_inj {α : Type u_1} {a b : α} {n : ℕ} (h : n ≠ 0) : replicate n a = replicate n b ↔ a = b

theorem Multiset.replicate_left_injective {α : Type u_1} (a : α) : Function.Injective fun (x : ℕ) => replicate x a

theorem Multiset.replicate_subset_singleton {α : Type u_1} (n : ℕ) (a : α) : replicate n a ⊆ {a}

theorem Multiset.replicate_le_coe {α : Type u_1} {a : α} {n : ℕ} {l : List α} : replicate n a ≤ ↑l ↔ (List.replicate n a).Sublist l

theorem Multiset.replicate_le_replicate {α : Type u_1} (a : α) {k n : ℕ} : replicate k a ≤ replicate n a ↔ k ≤ n

theorem Multiset.replicate_mono {α : Type u_1} (a : α) {k n : ℕ} (h : k ≤ n) : replicate k a ≤ replicate n a

theorem Multiset.le_replicate_iff {α : Type u_1} {m : Multiset α} {a : α} {n : ℕ} : m ≤ replicate n a ↔ ∃ (k : ℕ), k ≤ n ∧ m = replicate k a

theorem Multiset.lt_replicate_succ {α : Type u_1} {m : Multiset α} {x : α} {n : ℕ} : m < replicate (n + 1) x ↔ m ≤ replicate n x

Multiplicity of an element

@[simp]

theorem Multiset.count_replicate_self {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : count a (replicate n a) = n

theorem Multiset.count_replicate {α : Type u_1} [DecidableEq α] (a b : α) (n : ℕ) : count a (replicate n b) = if b = a then n else 0

theorem Multiset.le_count_iff_replicate_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {n : ℕ} : n ≤ count a s ↔ replicate n a ≤ s

Lift a relation to Multisets

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

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

theorem Multiset.nodup_iff_le {α : Type u_1} {s : Multiset α} : s.Nodup ↔ ∀ (a : α), ¬a ::ₘ a ::ₘ 0 ≤ s

theorem Multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : Multiset α} : s.Nodup ↔ ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t

theorem Multiset.nodup_iff_pairwise {α : Type u_3} {s : Multiset α} : s.Nodup ↔ Pairwise (fun (x1 x2 : α) => x1 ≠ x2) s

theorem Multiset.Nodup.pairwise {α : Type u_1} {r : α → α → Prop} {s : Multiset α} : (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≠ b → r a b) → s.Nodup → Pairwise r s