Definition of 0 and ::ₘ

This file defines constructors for multisets:

• Zero (Multiset α) instance: the empty multiset
• Multiset.cons: add one element to a multiset
• Singleton α (Multiset α) instance: multiset with one element

It also defines the following predicates on multisets:

• Multiset.Rel: Rel r s t lifts the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping between elements in s and t following r.

Notation

• 0: The empty multiset.
• {a}: The multiset containing a single occurrence of a.
• a ::ₘ s: The multiset containing one more occurrence of a than s does.

Main results

• Multiset.rec: recursion on adding one element to a multiset at a time.

Empty multiset

def Multiset.zero {α : Type u_1} : Multiset α

0 : Multiset α is the empty set

Equations

• Multiset.zero = ↑[]

@[instance_reducible]

instance Multiset.instZero {α : Type u_1} : Zero (Multiset α)

Equations

• Multiset.instZero = { zero := Multiset.zero }

@[instance_reducible]

instance Multiset.instEmptyCollection {α : Type u_1} : EmptyCollection (Multiset α)

Equations

• Multiset.instEmptyCollection = { emptyCollection := 0 }

@[instance_reducible]

instance Multiset.inhabitedMultiset {α : Type u_1} : Inhabited (Multiset α)

Equations

• Multiset.inhabitedMultiset = { default := 0 }

@[instance_reducible]

instance Multiset.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (Multiset α)

Equations

• Multiset.instUniqueOfIsEmpty = { default := 0, uniq := ⋯ }

@[simp]

theorem Multiset.coe_nil {α : Type u_1} : ↑[] = 0

@[simp]

theorem Multiset.empty_eq_zero {α : Type u_1} : ∅ = 0

@[simp]

theorem Multiset.coe_eq_zero {α : Type u_1} (l : List α) : ↑l = 0 ↔ l = []

theorem Multiset.coe_eq_zero_iff_isEmpty {α : Type u_1} (l : List α) : ↑l = 0 ↔ l.isEmpty = true

Multiset.cons

def Multiset.cons {α : Type u_1} (a : α) (s : Multiset α) : Multiset α

cons a s is the multiset which contains s plus one more instance of a.

Equations

• a ::ₘ s = Quot.liftOn s (fun (l : List α) => ↑(a :: l)) ⋯

def Multiset.«term_::ₘ_» : Lean.TrailingParserDescr

cons a s is the multiset which contains s plus one more instance of a.

Equations

• Multiset.«term_::ₘ_» = Lean.ParserDescr.trailingNode `Multiset.«term_::ₘ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₘ ") (Lean.ParserDescr.cat `term 67))

@[instance_reducible]

instance Multiset.instInsert {α : Type u_1} : Insert α (Multiset α)

Equations

• Multiset.instInsert = { insert := Multiset.cons }

@[simp]

theorem Multiset.insert_eq_cons {α : Type u_1} (a : α) (s : Multiset α) : insert a s = a ::ₘ s

@[simp]

theorem Multiset.cons_coe {α : Type u_1} (a : α) (l : List α) : a ::ₘ ↑l = ↑(a :: l)

@[simp]

theorem Multiset.cons_inj_left {α : Type u_1} {a b : α} (s : Multiset α) : a ::ₘ s = b ::ₘ s ↔ a = b

@[simp]

theorem Multiset.cons_inj_right {α : Type u_1} (a : α) {s t : Multiset α} : a ::ₘ s = a ::ₘ t ↔ s = t

theorem Multiset.induction {α : Type u_1} {p : Multiset α → Prop} (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) (s : Multiset α) : p s

theorem Multiset.induction_on {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α) (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : p s

theorem Multiset.cons_swap {α : Type u_1} (a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s

def Multiset.rec {α : Type u_1} {C : Multiset α → Sort u_3} (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)) (m : Multiset α) : C m

Dependent recursor on multisets. TODO: should be @[recursor 6], but then the definition of Multiset.pi fails with a stack overflow in whnf.

Equations

• Multiset.rec C_0 C_cons C_cons_heq m = Quotient.hrecOn m (List.rec C_0 fun (a : α) (l : List α) (b : C ⟦l⟧) => C_cons a ⟦l⟧ b) ⋯

def Multiset.recOn {α : Type u_1} {C : Multiset α → Sort u_3} (m : Multiset α) (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)) : C m

Companion to Multiset.rec with more convenient argument order.

Equations

• m.recOn C_0 C_cons C_cons_heq = Multiset.rec C_0 C_cons C_cons_heq m

@[simp]

theorem Multiset.recOn_0 {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)} : Multiset.recOn 0 C_0 C_cons C_cons_heq = C_0

@[simp]

theorem Multiset.recOn_cons {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)} (a : α) (m : Multiset α) : (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)

@[simp]

theorem Multiset.mem_cons {α : Type u_1} {a b : α} {s : Multiset α} : a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s

theorem Multiset.mem_cons_of_mem {α : Type u_1} {a b : α} {s : Multiset α} (h : a ∈ s) : a ∈ b ::ₘ s

theorem Multiset.mem_cons_self {α : Type u_1} (a : α) (s : Multiset α) : a ∈ a ::ₘ s

theorem Multiset.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {s : Multiset α} : (∀ (x : α), x ∈ a ::ₘ s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x

theorem Multiset.exists_cons_of_mem {α : Type u_1} {s : Multiset α} {a : α} : a ∈ s → ∃ (t : Multiset α), s = a ::ₘ t

@[simp]

theorem Multiset.notMem_zero {α : Type u_1} (a : α) : ¬a ∈ 0

theorem Multiset.eq_zero_of_forall_notMem {α : Type u_1} {s : Multiset α} : (∀ (x : α), ¬x ∈ s) → s = 0

theorem Multiset.eq_zero_iff_forall_notMem {α : Type u_1} {s : Multiset α} : s = 0 ↔ ∀ (a : α), ¬a ∈ s

theorem Multiset.exists_mem_of_ne_zero {α : Type u_1} {s : Multiset α} : s ≠ 0 → ∃ (a : α), a ∈ s

theorem Multiset.empty_or_exists_mem {α : Type u_1} (s : Multiset α) : s = 0 ∨ ∃ (a : α), a ∈ s

@[simp]

theorem Multiset.zero_ne_cons {α : Type u_1} {a : α} {m : Multiset α} : 0 ≠ a ::ₘ m

@[simp]

theorem Multiset.cons_ne_zero {α : Type u_1} {a : α} {m : Multiset α} : a ::ₘ m ≠ 0

theorem Multiset.cons_eq_cons {α : Type u_1} {a b : α} {as bs : Multiset α} : a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Singleton

@[instance_reducible]

instance Multiset.instSingleton {α : Type u_1} : Singleton α (Multiset α)

Equations

• Multiset.instSingleton = { singleton := fun (a : α) => a ::ₘ 0 }

instance Multiset.instLawfulSingleton {α : Type u_1} : LawfulSingleton α (Multiset α)

@[simp]

theorem Multiset.cons_zero {α : Type u_1} (a : α) : a ::ₘ 0 = {a}

@[simp]

theorem Multiset.coe_singleton {α : Type u_1} (a : α) : ↑[a] = {a}

@[simp]

theorem Multiset.mem_singleton {α : Type u_1} {a b : α} : b ∈ {a} ↔ b = a

theorem Multiset.mem_singleton_self {α : Type u_1} (a : α) : a ∈ {a}

@[simp]

theorem Multiset.singleton_inj {α : Type u_1} {a b : α} : {a} = {b} ↔ a = b

@[simp]

theorem Multiset.coe_eq_singleton {α : Type u_1} {l : List α} {a : α} : ↑l = {a} ↔ l = [a]

@[simp]

theorem Multiset.singleton_eq_cons_iff {α : Type u_1} {a b : α} (m : Multiset α) : {a} = b ::ₘ m ↔ a = b ∧ m = 0

theorem Multiset.pair_comm {α : Type u_1} (x y : α) : {x, y} = {y, x}

Multiset.Subset

@[simp]

theorem Multiset.zero_subset {α : Type u_1} (s : Multiset α) : 0 ⊆ s

theorem Multiset.subset_cons {α : Type u_1} (s : Multiset α) (a : α) : s ⊆ a ::ₘ s

theorem Multiset.ssubset_cons {α : Type u_1} {s : Multiset α} {a : α} (ha : ¬a ∈ s) : s ⊂ a ::ₘ s

@[simp]

theorem Multiset.cons_subset {α : Type u_1} {a : α} {s t : Multiset α} : a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

theorem Multiset.cons_subset_cons {α : Type u_1} {a : α} {s t : Multiset α} : s ⊆ t → a ::ₘ s ⊆ a ::ₘ t

theorem Multiset.eq_zero_of_subset_zero {α : Type u_1} {s : Multiset α} (h : s ⊆ 0) : s = 0

@[simp]

theorem Multiset.subset_zero {α : Type u_1} {s : Multiset α} : s ⊆ 0 ↔ s = 0

@[simp]

theorem Multiset.zero_ssubset {α : Type u_1} {s : Multiset α} : 0 ⊂ s ↔ s ≠ 0

@[simp]

theorem Multiset.singleton_subset {α : Type u_1} {s : Multiset α} {a : α} : {a} ⊆ s ↔ a ∈ s

theorem Multiset.induction_on' {α : Type u_1} {p : Multiset α → Prop} (S : Multiset α) (h₁ : p 0) (h₂ : ∀ {a : α} {s : Multiset α}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S

Partial order on Multisets

theorem Multiset.zero_le {α : Type u_1} (s : Multiset α) : 0 ≤ s

@[instance_reducible]

instance Multiset.instOrderBot {α : Type u_1} : OrderBot (Multiset α)

Equations

• Multiset.instOrderBot = { bot := 0, bot_le := ⋯ }

@[simp]

theorem Multiset.bot_eq_zero {α : Type u_1} : ⊥ = 0

This is a rfl and simp version of bot_eq_zero.

theorem Multiset.le_zero {α : Type u_1} {s : Multiset α} : s ≤ 0 ↔ s = 0

theorem Multiset.lt_cons_self {α : Type u_1} (s : Multiset α) (a : α) : s < a ::ₘ s

theorem Multiset.le_cons_self {α : Type u_1} (s : Multiset α) (a : α) : s ≤ a ::ₘ s

@[simp]

theorem Multiset.cons_le_cons_iff {α : Type u_1} {s t : Multiset α} (a : α) : a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t

theorem Multiset.cons_le_cons {α : Type u_1} {s t : Multiset α} (a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t

@[simp]

theorem Multiset.cons_lt_cons_iff {α : Type u_1} {s t : Multiset α} {a : α} : a ::ₘ s < a ::ₘ t ↔ s < t

theorem Multiset.cons_lt_cons {α : Type u_1} {s t : Multiset α} (a : α) (h : s < t) : a ::ₘ s < a ::ₘ t

theorem Multiset.le_cons_of_notMem {α : Type u_1} {s t : Multiset α} {a : α} (m : ¬a ∈ s) : s ≤ a ::ₘ t ↔ s ≤ t

theorem Multiset.cons_le_of_notMem {α : Type u_1} {s t : Multiset α} {a : α} (hs : ¬a ∈ s) : a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

@[simp]

theorem Multiset.singleton_ne_zero {α : Type u_1} (a : α) : {a} ≠ 0

@[simp]

theorem Multiset.zero_ne_singleton {α : Type u_1} (a : α) : 0 ≠ {a}

@[simp]

theorem Multiset.singleton_le {α : Type u_1} {a : α} {s : Multiset α} : {a} ≤ s ↔ a ∈ s

@[simp]

theorem Multiset.le_singleton {α : Type u_1} {s : Multiset α} {a : α} : s ≤ {a} ↔ s = 0 ∨ s = {a}

@[simp]

theorem Multiset.lt_singleton {α : Type u_1} {s : Multiset α} {a : α} : s < {a} ↔ s = 0

@[simp]

theorem Multiset.ssubset_singleton_iff {α : Type u_1} {s : Multiset α} {a : α} : s ⊂ {a} ↔ s = 0

Cardinality

@[simp]

theorem Multiset.card_zero {α : Type u_1} : card 0 = 0

@[simp]

theorem Multiset.card_cons {α : Type u_1} (a : α) (s : Multiset α) : (a ::ₘ s).card = s.card + 1

@[simp]

theorem Multiset.card_singleton {α : Type u_1} (a : α) : {a}.card = 1

theorem Multiset.card_pair {α : Type u_1} (a b : α) : {a, b}.card = 2

theorem Multiset.card_eq_one {α : Type u_1} {s : Multiset α} : s.card = 1 ↔ ∃ (a : α), s = {a}

theorem Multiset.lt_iff_cons_le {α : Type u_1} {s t : Multiset α} : s < t ↔ ∃ (a : α), a ::ₘ s ≤ t

@[simp]

theorem Multiset.card_eq_zero {α : Type u_1} {s : Multiset α} : s.card = 0 ↔ s = 0

theorem Multiset.card_pos {α : Type u_1} {s : Multiset α} : 0 < s.card ↔ s ≠ 0

theorem Multiset.card_pos_iff_exists_mem {α : Type u_1} {s : Multiset α} : 0 < s.card ↔ ∃ (a : α), a ∈ s

theorem Multiset.card_eq_two {α : Type u_1} {s : Multiset α} : s.card = 2 ↔ ∃ (x : α), ∃ (y : α), s = {x, y}

theorem Multiset.card_eq_three {α : Type u_1} {s : Multiset α} : s.card = 3 ↔ ∃ (x : α), ∃ (y : α), ∃ (z : α), s = {x, y, z}

theorem Multiset.card_eq_four {α : Type u_1} {s : Multiset α} : s.card = 4 ↔ ∃ (x : α), ∃ (y : α), ∃ (z : α), ∃ (w : α), s = {x, y, z, w}

theorem Multiset.card_eq_succ_iff {α : Type u_1} {s : Multiset α} {n : ℕ} : s.card = n + 1 ↔ ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n

Map for partial functions

@[simp]

theorem Multiset.pmap_zero {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (h : ∀ (a : α), a ∈ 0 → p a) : pmap f 0 h = 0

@[simp]

theorem Multiset.pmap_cons {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (m : Multiset α) (h : ∀ (b : α), b ∈ a ::ₘ m → p b) : pmap f (a ::ₘ m) h = f a ⋯ ::ₘ pmap f m ⋯

@[simp]

theorem Multiset.attach_zero {α : Type u_1} : attach 0 = 0

Lift a relation to Multisets

inductive Multiset.Rel {α : Type u_1} {β : Type v} (r : α → β → Prop) : Multiset α → Multiset β → Prop

Rel r s t -- lift the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping between elements in s and t following r.

• zero {α : Type u_1} {β : Type v} {r : α → β → Prop} : Rel r 0 0
• cons {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {b : β} {as : Multiset α} {bs : Multiset β} : r a b → Rel r as bs → Rel r (a ::ₘ as) (b ::ₘ bs)

theorem Multiset.rel_iff {α : Type u_1} {β : Type v} (r : α → β → Prop) (a✝ : Multiset α) (a✝¹ : Multiset β) : Rel r a✝ a✝¹ ↔ a✝ = 0 ∧ a✝¹ = 0 ∨ ∃ (a : α), ∃ (b : β), ∃ (as : Multiset α), ∃ (bs : Multiset β), r a b ∧ Rel r as bs ∧ a✝ = a ::ₘ as ∧ a✝¹ = b ::ₘ bs

theorem Multiset.rel_flip {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset β} {t : Multiset α} : Rel (flip r) s t ↔ Rel r t s

theorem Multiset.rel_refl_of_refl_on {α : Type u_1} {m : Multiset α} {r : α → α → Prop} : (∀ (x : α), x ∈ m → r x x) → Rel r m m

theorem Multiset.rel_eq_refl {α : Type u_1} {s : Multiset α} : Rel (fun (x1 x2 : α) => x1 = x2) s s

theorem Multiset.rel_eq {α : Type u_1} {s t : Multiset α} : Rel (fun (x1 x2 : α) => x1 = x2) s t ↔ s = t

theorem Multiset.Rel.mono {α : Type u_1} {β : Type v} {r p : α → β → Prop} {s : Multiset α} {t : Multiset β} (hst : Rel r s t) (h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) : Rel p s t

theorem Multiset.rel_flip_eq {α : Type u_1} {s t : Multiset α} : Rel (fun (a b : α) => b = a) s t ↔ s = t

@[simp]

theorem Multiset.rel_zero_left {α : Type u_1} {β : Type v} {r : α → β → Prop} {b : Multiset β} : Rel r 0 b ↔ b = 0

@[simp]

theorem Multiset.rel_zero_right {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : Multiset α} : Rel r a 0 ↔ a = 0

theorem Multiset.rel_cons_left {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {as : Multiset α} {bs : Multiset β} : Rel r (a ::ₘ as) bs ↔ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

theorem Multiset.rel_cons_right {α : Type u_1} {β : Type v} {r : α → β → Prop} {as : Multiset α} {b : β} {bs : Multiset β} : Rel r as (b ::ₘ bs) ↔ ∃ (a : α), ∃ (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

theorem Multiset.card_eq_card_of_rel {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) : s.card = t.card

theorem Multiset.exists_mem_of_rel_of_mem {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) {a : α} : a ∈ s → ∃ (b : β), b ∈ t ∧ r a b

theorem Multiset.rel_of_forall {α : Type u_1} {m1 m2 : Multiset α} {r : α → α → Prop} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card) : Rel r m1 m2

theorem Multiset.Rel.trans {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u) : Rel r s u

@[simp]

theorem Multiset.pairwise_zero {α : Type u_1} (r : α → α → Prop) : Pairwise r 0

@[simp]

theorem Multiset.nodup_zero {α : Type u_1} : Nodup 0

@[simp]

theorem Multiset.nodup_cons {α : Type u_1} {a : α} {s : Multiset α} : (a ::ₘ s).Nodup ↔ ¬a ∈ s ∧ s.Nodup

theorem Multiset.Nodup.cons {α : Type u_1} {s : Multiset α} {a : α} (m : ¬a ∈ s) (n : s.Nodup) : (a ::ₘ s).Nodup

theorem Multiset.Nodup.of_cons {α : Type u_1} {s : Multiset α} {a : α} (h : (a ::ₘ s).Nodup) : s.Nodup

theorem Multiset.Nodup.notMem {α : Type u_1} {s : Multiset α} {a : α} (h : (a ::ₘ s).Nodup) : ¬a ∈ s