Documentation

def Multiset.zero {α : Type u_1} :

Multiset α

0 : Multiset α is the empty set

Instances For

@[implicit_reducible]

instance Multiset.instZero {α : Type u_1} :

Zero (Multiset α)

@[implicit_reducible]

instance Multiset.instEmptyCollection {α : Type u_1} :

EmptyCollection (Multiset α)

@[implicit_reducible]

instance Multiset.inhabitedMultiset {α : Type u_1} :

Inhabited (Multiset α)

@[implicit_reducible]

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

Unique (Multiset α)

@[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.

Instances For

def Multiset.«term_::ₘ_» :

Lean.TrailingParserDescr

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

Instances For

@[implicit_reducible]

instance Multiset.instInsert {α : Type u_1} :

Insert α (Multiset α)

@[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.

Instances For

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.

Instances For

@[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 ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ 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 #

@[implicit_reducible]

instance Multiset.instSingleton {α : Type u_1} :

Singleton α (Multiset α)

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 `Multiset`s #

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

0 ≤ s

@[implicit_reducible]

instance Multiset.instOrderBot {α : Type u_1} :

OrderBot (Multiset α)

@[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}

Map for partial functions #

@[simp]

theorem Multiset.pmap_zero {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (h : ∀ 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 ∈ 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 `Multiset`s #

🔶 coverage

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)

Instances For

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 ∈ 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 ∈ s, ∀ 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 ∈ 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