data.multiset.basic - mathlib3 docs

theorem multiset.induction_on {α : Type u_1} {p : multiset α → Prop} (s : multiset α) (h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p s → p (a ::ₘ s)) :

p s

source

theorem multiset.cons_swap {α : Type u_1} (a b : α) (s : multiset α) :

a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s

source

@[protected]

def multiset.rec {α : Type u_1} {C : multiset α → Sort u_4} (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.hrec_on m (list.rec C_0 (λ (a : α) (l : list α) (b : (λ (l : list α), C ⟦l⟧) l), C_cons a ⟦l⟧ b)) _

source

@[protected]

def multiset.rec_on {α : Type u_1} {C : multiset α → Sort u_4} (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.rec_on C_0 C_cons C_cons_heq = multiset.rec C_0 C_cons C_cons_heq m

source

@[simp]

theorem multiset.rec_on_0 {α : Type u_1} {C : multiset α → Sort u_4} {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)} :

0.rec_on C_0 C_cons C_cons_heq = C_0

source

@[simp]

theorem multiset.rec_on_cons {α : Type u_1} {C : multiset α → Sort u_4} {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).rec_on C_0 C_cons C_cons_heq = C_cons a m (m.rec_on C_0 C_cons C_cons_heq)

source

def multiset.mem {α : Type u_1} (a : α) (s : multiset α) :

Prop

a ∈ s means that a has nonzero multiplicity in s.

Equations

multiset.mem a s = quot.lift_on s (λ (l : list α), a ∈ l) _

source

@[protected, instance]

def multiset.has_mem {α : Type u_1} :

has_mem α (multiset α)

Equations

multiset.has_mem = {mem := multiset.mem α}

source

@[simp]

theorem multiset.mem_coe {α : Type u_1} {a : α} {l : list α} :

a ∈ ↑l ↔ a ∈ l

source

@[protected, instance]

def multiset.decidable_mem {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

decidable (a ∈ s)

Equations

multiset.decidable_mem a s = quot.rec_on_subsingleton s (list.decidable_mem a)

source

@[simp]

theorem multiset.mem_cons {α : Type u_1} {a b : α} {s : multiset α} :

a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s

source

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

a ∈ b ::ₘ s

source

@[simp]

theorem multiset.mem_cons_self {α : Type u_1} (a : α) (s : multiset α) :

a ∈ a ::ₘ s

source

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

source

theorem multiset.exists_cons_of_mem {α : Type u_1} {s : multiset α} {a : α} :

a ∈ s → (∃ (t : multiset α), s = a ::ₘ t)

source

@[simp]

theorem multiset.not_mem_zero {α : Type u_1} (a : α) :

a ∉ 0

source

theorem multiset.eq_zero_of_forall_not_mem {α : Type u_1} {s : multiset α} :

(∀ (x : α), x ∉ s) → s = 0

source

theorem multiset.eq_zero_iff_forall_not_mem {α : Type u_1} {s : multiset α} :

s = 0 ↔ ∀ (a : α), a ∉ s

source

theorem multiset.exists_mem_of_ne_zero {α : Type u_1} {s : multiset α} :

s ≠ 0 → (∃ (a : α), a ∈ s)

source

theorem multiset.empty_or_exists_mem {α : Type u_1} (s : multiset α) :

s = 0 ∨ ∃ (a : α), a ∈ s

source

@[simp]

theorem multiset.zero_ne_cons {α : Type u_1} {a : α} {m : multiset α} :

0 ≠ a ::ₘ m

source

@[simp]

theorem multiset.cons_ne_zero {α : Type u_1} {a : α} {m : multiset α} :

a ::ₘ m ≠ 0

source

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

source

@[protected, instance]

def multiset.has_singleton {α : Type u_1} :

has_singleton α (multiset α)

Equations

multiset.has_singleton = {singleton := λ (a : α), a ::ₘ 0}

source

@[protected, instance]

def multiset.is_lawful_singleton {α : Type u_1} :

is_lawful_singleton α (multiset α)

source

@[simp]

theorem multiset.cons_zero {α : Type u_1} (a : α) :

a ::ₘ 0 = {a}

source

@[simp, norm_cast]

theorem multiset.coe_singleton {α : Type u_1} (a : α) :

↑[a] = {a}

source

@[simp]

theorem multiset.mem_singleton {α : Type u_1} {a b : α} :

b ∈ {a} ↔ b = a

source

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

a ∈ {a}

source

@[simp]

theorem multiset.singleton_inj {α : Type u_1} {a b : α} :

{a} = {b} ↔ a = b

source

@[simp, norm_cast]

theorem multiset.coe_eq_singleton {α : Type u_1} {l : list α} {a : α} :

↑l = {a} ↔ l = [a]

source

@[simp]

theorem multiset.singleton_eq_cons_iff {α : Type u_1} {a b : α} (m : multiset α) :

{a} = b ::ₘ m ↔ a = b ∧ m = 0

source

theorem multiset.pair_comm {α : Type u_1} (x y : α) :

{x, y} = {y, x}

source

@[protected]

def multiset.subset {α : Type u_1} (s t : multiset α) :

Prop

s ⊆ t is the lift of the list subset relation. It means that any element with nonzero multiplicity in s has nonzero multiplicity in t, but it does not imply that the multiplicity of a in s is less or equal than in t; see s ≤ t for this relation.

Equations

s.subset t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t

source

@[protected, instance]

def multiset.has_subset {α : Type u_1} :

has_subset (multiset α)

Equations

multiset.has_subset = {subset := multiset.subset α}

source

@[protected, instance]

def multiset.has_ssubset {α : Type u_1} :

has_ssubset (multiset α)

Equations

multiset.has_ssubset = {ssubset := λ (s t : multiset α), s ⊆ t ∧ ¬t ⊆ s}

source

@[simp]

theorem multiset.coe_subset {α : Type u_1} {l₁ l₂ : list α} :

↑l₁ ⊆ ↑l₂ ↔ l₁ ⊆ l₂

source

@[simp]

theorem multiset.subset.refl {α : Type u_1} (s : multiset α) :

s ⊆ s

source

theorem multiset.subset.trans {α : Type u_1} {s t u : multiset α} :

s ⊆ t → t ⊆ u → s ⊆ u

source

theorem multiset.subset_iff {α : Type u_1} {s t : multiset α} :

s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t

source

theorem multiset.mem_of_subset {α : Type u_1} {s t : multiset α} {a : α} (h : s ⊆ t) :

a ∈ s → a ∈ t

source

@[simp]

theorem multiset.zero_subset {α : Type u_1} (s : multiset α) :

0 ⊆ s

source

theorem multiset.subset_cons {α : Type u_1} (s : multiset α) (a : α) :

s ⊆ a ::ₘ s

source

theorem multiset.ssubset_cons {α : Type u_1} {s : multiset α} {a : α} (ha : a ∉ s) :

s ⊂ a ::ₘ s

source

@[simp]

theorem multiset.cons_subset {α : Type u_1} {a : α} {s t : multiset α} :

a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

source

theorem multiset.cons_subset_cons {α : Type u_1} {a : α} {s t : multiset α} :

s ⊆ t → a ::ₘ s ⊆ a ::ₘ t

source

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

s = 0

source

theorem multiset.subset_zero {α : Type u_1} {s : multiset α} :

s ⊆ 0 ↔ s = 0

source

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 (has_insert.insert a s)) :

p S

source

noncomputable def multiset.to_list {α : Type u_1} (s : multiset α) :

list α

Produces a list of the elements in the multiset using choice.

Equations

s.to_list = quotient.out' s

source

@[simp, norm_cast]

theorem multiset.coe_to_list {α : Type u_1} (s : multiset α) :

↑(s.to_list) = s

source

@[simp]

theorem multiset.to_list_eq_nil {α : Type u_1} {s : multiset α} :

s.to_list = list.nil ↔ s = 0

source

@[simp]

theorem multiset.empty_to_list {α : Type u_1} {s : multiset α} :

↥(s.to_list.empty) ↔ s = 0

source

@[simp]

theorem multiset.to_list_zero {α : Type u_1} :

0.to_list = list.nil

source

@[simp]

theorem multiset.mem_to_list {α : Type u_1} {a : α} {s : multiset α} :

a ∈ s.to_list ↔ a ∈ s

source

@[simp]

theorem multiset.to_list_eq_singleton_iff {α : Type u_1} {a : α} {m : multiset α} :

m.to_list = [a] ↔ m = {a}

source

@[simp]

theorem multiset.to_list_singleton {α : Type u_1} (a : α) :

{a}.to_list = [a]

source

@[protected]

def multiset.le {α : Type u_1} (s t : multiset α) :

Prop

s ≤ t means that s is a sublist of t (up to permutation). Equivalently, s ≤ t means that count a s ≤ count a t for all a.

Equations

s.le t = quotient.lift_on₂ s t list.subperm multiset.le._proof_1

source

@[protected, instance]

def multiset.partial_order {α : Type u_1} :

partial_order (multiset α)

Equations

multiset.partial_order = {le := multiset.le α, lt := preorder.lt._default multiset.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def multiset.decidable_le {α : Type u_1} [decidable_eq α] :

decidable_rel has_le.le

Equations

multiset.decidable_le = λ (s t : multiset α), quotient.rec_on_subsingleton₂ s t list.decidable_subperm

source

theorem multiset.subset_of_le {α : Type u_1} {s t : multiset α} :

s ≤ t → s ⊆ t

source

theorem multiset.le.subset {α : Type u_1} {s t : multiset α} :

s ≤ t → s ⊆ t

Alias of multiset.subset_of_le.

source

theorem multiset.mem_of_le {α : Type u_1} {s t : multiset α} {a : α} (h : s ≤ t) :

a ∈ s → a ∈ t

source

theorem multiset.not_mem_mono {α : Type u_1} {s t : multiset α} {a : α} (h : s ⊆ t) :

a ∉ t → a ∉ s

source

@[simp]

theorem multiset.coe_le {α : Type u_1} {l₁ l₂ : list α} :

↑l₁ ≤ ↑l₂ ↔ l₁ <+~ l₂

source

theorem multiset.le_induction_on {α : Type u_1} {C : multiset α → multiset α → Prop} {s t : multiset α} (h : s ≤ t) (H : ∀ {l₁ l₂ : list α}, l₁ <+ l₂ → C ↑l₁ ↑l₂) :

C s t

source

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

0 ≤ s

source

@[protected, instance]

def multiset.order_bot {α : Type u_1} :

order_bot (multiset α)

Equations

multiset.order_bot = {bot := 0, bot_le := _}

source

@[simp]

theorem multiset.bot_eq_zero {α : Type u_1} :

⊥ = 0

This is a rfl and simp version of bot_eq_zero.

source

theorem multiset.le_zero {α : Type u_1} {s : multiset α} :

s ≤ 0 ↔ s = 0

source

theorem multiset.lt_cons_self {α : Type u_1} (s : multiset α) (a : α) :

s < a ::ₘ s

source

theorem multiset.le_cons_self {α : Type u_1} (s : multiset α) (a : α) :

s ≤ a ::ₘ s

source

theorem multiset.cons_le_cons_iff {α : Type u_1} {s t : multiset α} (a : α) :

a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t

source

theorem multiset.cons_le_cons {α : Type u_1} {s t : multiset α} (a : α) :

s ≤ t → a ::ₘ s ≤ a ::ₘ t

source

theorem multiset.le_cons_of_not_mem {α : Type u_1} {s t : multiset α} {a : α} (m : a ∉ s) :

s ≤ a ::ₘ t ↔ s ≤ t

source

@[simp]

theorem multiset.singleton_ne_zero {α : Type u_1} (a : α) :

{a} ≠ 0

source

@[simp]

theorem multiset.singleton_le {α : Type u_1} {a : α} {s : multiset α} :

{a} ≤ s ↔ a ∈ s

source

@[protected]

def multiset.add {α : Type u_1} (s₁ s₂ : multiset α) :

multiset α

The sum of two multisets is the lift of the list append operation. This adds the multiplicities of each element, i.e. count a (s + t) = count a s + count a t.

Equations

s₁.add s₂ = quotient.lift_on₂ s₁ s₂ (λ (l₁ l₂ : list α), ↑(l₁ ++ l₂)) multiset.add._proof_1

source

@[protected, instance]

def multiset.has_add {α : Type u_1} :

has_add (multiset α)

Equations

multiset.has_add = {add := multiset.add α}

source

@[simp]

theorem multiset.coe_add {α : Type u_1} (s t : list α) :

↑s + ↑t = ↑(s ++ t)

source

@[simp]

theorem multiset.singleton_add {α : Type u_1} (a : α) (s : multiset α) :

{a} + s = a ::ₘ s

source

@[protected, instance]

def multiset.has_le.le.covariant_class {α : Type u_1} :

covariant_class (multiset α) (multiset α) has_add.add has_le.le

source

@[protected, instance]

def multiset.has_le.le.contravariant_class {α : Type u_1} :

contravariant_class (multiset α) (multiset α) has_add.add has_le.le

source

@[protected, instance]

def multiset.ordered_cancel_add_comm_monoid {α : Type u_1} :

ordered_cancel_add_comm_monoid (multiset α)

Equations

multiset.ordered_cancel_add_comm_monoid = {add := has_add.add multiset.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul._default 0 has_add.add multiset.ordered_cancel_add_comm_monoid._proof_4 multiset.ordered_cancel_add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le multiset.partial_order, lt := partial_order.lt multiset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}

source

theorem multiset.le_add_right {α : Type u_1} (s t : multiset α) :

s ≤ s + t

source

theorem multiset.le_add_left {α : Type u_1} (s t : multiset α) :

s ≤ t + s

source

theorem multiset.le_iff_exists_add {α : Type u_1} {s t : multiset α} :

s ≤ t ↔ ∃ (u : multiset α), t = s + u

source

@[protected, instance]

def multiset.canonically_ordered_add_monoid {α : Type u_1} :

canonically_ordered_add_monoid (multiset α)

Equations

source

@[simp]

theorem multiset.cons_add {α : Type u_1} (a : α) (s t : multiset α) :

a ::ₘ s + t = a ::ₘ (s + t)

source

@[simp]

theorem multiset.add_cons {α : Type u_1} (a : α) (s t : multiset α) :

s + a ::ₘ t = a ::ₘ (s + t)

source

@[simp]

theorem multiset.mem_add {α : Type u_1} {a : α} {s t : multiset α} :

a ∈ s + t ↔ a ∈ s ∨ a ∈ t

source

theorem multiset.mem_of_mem_nsmul {α : Type u_1} {a : α} {s : multiset α} {n : ℕ} (h : a ∈ n • s) :

a ∈ s

source

@[simp]

theorem multiset.mem_nsmul {α : Type u_1} {a : α} {s : multiset α} {n : ℕ} (h0 : n ≠ 0) :

a ∈ n • s ↔ a ∈ s

source

theorem multiset.nsmul_cons {α : Type u_1} {s : multiset α} (n : ℕ) (a : α) :

n • (a ::ₘ s) = n • {a} + n • s

source

def multiset.card {α : Type u_1} :

multiset α →+ ℕ

The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.

Equations

multiset.card = {to_fun := λ (s : multiset α), quot.lift_on s list.length multiset.card._proof_1, map_zero' := _, map_add' := _}

source

@[simp]

theorem multiset.coe_card {α : Type u_1} (l : list α) :

⇑multiset.card ↑l = l.length

source

@[simp]

theorem multiset.length_to_list {α : Type u_1} (s : multiset α) :

s.to_list.length = ⇑multiset.card s

source

@[simp]

theorem multiset.card_zero {α : Type u_1} :

⇑multiset.card 0 = 0

source

theorem multiset.card_add {α : Type u_1} (s t : multiset α) :

⇑multiset.card (s + t) = ⇑multiset.card s + ⇑multiset.card t

source

theorem multiset.card_nsmul {α : Type u_1} (s : multiset α) (n : ℕ) :

⇑multiset.card (n • s) = n * ⇑multiset.card s

source

@[simp]

theorem multiset.card_cons {α : Type u_1} (a : α) (s : multiset α) :

⇑multiset.card (a ::ₘ s) = ⇑multiset.card s + 1

source

@[simp]

theorem multiset.card_singleton {α : Type u_1} (a : α) :

⇑multiset.card {a} = 1

source

theorem multiset.card_pair {α : Type u_1} (a b : α) :

⇑multiset.card {a, b} = 2

source

theorem multiset.card_eq_one {α : Type u_1} {s : multiset α} :

⇑multiset.card s = 1 ↔ ∃ (a : α), s = {a}

source

theorem multiset.card_le_of_le {α : Type u_1} {s t : multiset α} (h : s ≤ t) :

⇑multiset.card s ≤ ⇑multiset.card t

source

theorem multiset.card_mono {α : Type u_1} :

monotone ⇑multiset.card

source

theorem multiset.eq_of_le_of_card_le {α : Type u_1} {s t : multiset α} (h : s ≤ t) :

⇑multiset.card t ≤ ⇑multiset.card s → s = t

source

theorem multiset.card_lt_of_lt {α : Type u_1} {s t : multiset α} (h : s < t) :

⇑multiset.card s < ⇑multiset.card t

source

theorem multiset.lt_iff_cons_le {α : Type u_1} {s t : multiset α} :

s < t ↔ ∃ (a : α), a ::ₘ s ≤ t

source

@[simp]

theorem multiset.card_eq_zero {α : Type u_1} {s : multiset α} :

⇑multiset.card s = 0 ↔ s = 0

source

theorem multiset.card_pos {α : Type u_1} {s : multiset α} :

0 < ⇑multiset.card s ↔ s ≠ 0

source

theorem multiset.card_pos_iff_exists_mem {α : Type u_1} {s : multiset α} :

0 < ⇑multiset.card s ↔ ∃ (a : α), a ∈ s

source

theorem multiset.card_eq_two {α : Type u_1} {s : multiset α} :

⇑multiset.card s = 2 ↔ ∃ (x y : α), s = {x, y}

source

theorem multiset.card_eq_three {α : Type u_1} {s : multiset α} :

⇑multiset.card s = 3 ↔ ∃ (x y z : α), s = {x, y, z}

source

def multiset.strong_induction_on {α : Type u_1} {p : multiset α → Sort u_2} (s : multiset α) :

(Π (s : multiset α), (Π (t : multiset α), t < s → p t) → p s) → p s

A strong induction principle for multisets: If you construct a value for a particular multiset given values for all strictly smaller multisets, you can construct a value for any multiset.

Equations

s.strong_induction_on = λ (ih : Π (s : multiset α), (Π (t : multiset α), t < s → p t) → p s), ih s (λ (t : multiset α) (h : t < s), t.strong_induction_on ih)

source

theorem multiset.strong_induction_eq {α : Type u_1} {p : multiset α → Sort u_2} (s : multiset α) (H : Π (s : multiset α), (Π (t : multiset α), t < s → p t) → p s) :

s.strong_induction_on H = H s (λ (t : multiset α) (h : t < s), t.strong_induction_on H)

source

theorem multiset.case_strong_induction_on {α : Type u_1} {p : multiset α → Prop} (s : multiset α) (h₀ : p 0) (h₁ : ∀ (a : α) (s : multiset α), (∀ (t : multiset α), t ≤ s → p t) → p (a ::ₘ s)) :

p s

source

def multiset.strong_downward_induction {α : Type u_1} {p : multiset α → Sort u_2} {n : ℕ} (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁) (s : multiset α) :

⇑multiset.card s ≤ n → p s

Suppose that, given that p t can be defined on all supersets of s of cardinality less than n, one knows how to define p s. Then one can inductively define p s for all multisets s of cardinality less than n, starting from multisets of card n and iterating. This can be used either to define data, or to prove properties.

Equations

multiset.strong_downward_induction H s = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (h : s < t), multiset.strong_downward_induction H t ht)

source

theorem multiset.strong_downward_induction_eq {α : Type u_1} {p : multiset α → Sort u_2} {n : ℕ} (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁) (s : multiset α) :

multiset.strong_downward_induction H s = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (hst : s < t), multiset.strong_downward_induction H t ht)

source

def multiset.strong_downward_induction_on {α : Type u_1} {p : multiset α → Sort u_2} {n : ℕ} (s : multiset α) :

(Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁) → ⇑multiset.card s ≤ n → p s

Analogue of strong_downward_induction with order of arguments swapped.

Equations

multiset.strong_downward_induction_on = λ (s : multiset α) (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁), multiset.strong_downward_induction H s

source

theorem multiset.strong_downward_induction_on_eq {α : Type u_1} {p : multiset α → Sort u_2} (s : multiset α) {n : ℕ} (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁) :

s.strong_downward_induction_on H = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (h : s < t), t.strong_downward_induction_on H ht)

source

theorem multiset.well_founded_lt {α : Type u_1} :

well_founded has_lt.lt

Another way of expressing strong_induction_on: the (<) relation is well-founded.

source

@[protected, instance]

def multiset.is_well_founded_lt {α : Type u_1} :

well_founded_lt (multiset α)

source

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)

source

theorem multiset.coe_replicate {α : Type u_1} (n : ℕ) (a : α) :

↑(list.replicate n a) = multiset.replicate n a

source

@[simp]

theorem multiset.replicate_zero {α : Type u_1} (a : α) :

multiset.replicate 0 a = 0

source

@[simp]

theorem multiset.replicate_succ {α : Type u_1} (a : α) (n : ℕ) :

multiset.replicate (n + 1) a = a ::ₘ multiset.replicate n a

source

theorem multiset.replicate_add {α : Type u_1} (m n : ℕ) (a : α) :

multiset.replicate (m + n) a = multiset.replicate m a + multiset.replicate n a

source

def multiset.replicate_add_monoid_hom {α : Type u_1} (a : α) :

ℕ →+ multiset α

multiset.replicate as an add_monoid_hom.

Equations

multiset.replicate_add_monoid_hom a = {to_fun := λ (n : ℕ), multiset.replicate n a, map_zero' := _, map_add' := _}

source

@[simp]

theorem multiset.replicate_add_monoid_hom_apply {α : Type u_1} (a : α) (n : ℕ) :

⇑(multiset.replicate_add_monoid_hom a) n = multiset.replicate n a

source

theorem multiset.replicate_one {α : Type u_1} (a : α) :

multiset.replicate 1 a = {a}

source

@[simp]

theorem multiset.card_replicate {α : Type u_1} (n : ℕ) (a : α) :

⇑multiset.card (multiset.replicate n a) = n

source

theorem multiset.mem_replicate {α : Type u_1} {a b : α} {n : ℕ} :

b ∈ multiset.replicate n a ↔ n ≠ 0 ∧ b = a

source

theorem multiset.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : ℕ} :

b ∈ multiset.replicate n a → b = a

source

theorem multiset.eq_replicate_card {α : Type u_1} {a : α} {s : multiset α} :

s = multiset.replicate (⇑multiset.card s) a ↔ ∀ (b : α), b ∈ s → b = a

source

theorem multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : multiset α} :

(∀ (b : α), b ∈ s → b = a) → s = multiset.replicate (⇑multiset.card s) a

Alias of the reverse direction of multiset.eq_replicate_card.

source

theorem multiset.eq_replicate {α : Type u_1} {a : α} {n : ℕ} {s : multiset α} :

s = multiset.replicate n a ↔ ⇑multiset.card s = n ∧ ∀ (b : α), b ∈ s → b = a

source

theorem multiset.replicate_right_injective {α : Type u_1} {n : ℕ} (hn : n ≠ 0) :

function.injective (multiset.replicate n)

source

@[simp]

theorem multiset.replicate_right_inj {α : Type u_1} {a b : α} {n : ℕ} (h : n ≠ 0) :

multiset.replicate n a = multiset.replicate n b ↔ a = b

source

theorem multiset.replicate_left_injective {α : Type u_1} (a : α) :

function.injective (λ (n : ℕ), multiset.replicate n a)

source

theorem multiset.replicate_subset_singleton {α : Type u_1} (n : ℕ) (a : α) :

multiset.replicate n a ⊆ {a}

source

theorem multiset.replicate_le_coe {α : Type u_1} {a : α} {n : ℕ} {l : list α} :

multiset.replicate n a ≤ ↑l ↔ list.replicate n a <+ l

source

theorem multiset.nsmul_singleton {α : Type u_1} (a : α) (n : ℕ) :

n • {a} = multiset.replicate n a

source

theorem multiset.nsmul_replicate {α : Type u_1} {a : α} (n m : ℕ) :

n • multiset.replicate m a = multiset.replicate (n * m) a

source

theorem multiset.replicate_le_replicate {α : Type u_1} (a : α) {k n : ℕ} :

multiset.replicate k a ≤ multiset.replicate n a ↔ k ≤ n

source

theorem multiset.le_replicate_iff {α : Type u_1} {m : multiset α} {a : α} {n : ℕ} :

m ≤ multiset.replicate n a ↔ ∃ (k : ℕ) (H : k ≤ n), m = multiset.replicate k a

source

theorem multiset.lt_replicate_succ {α : Type u_1} {m : multiset α} {x : α} {n : ℕ} :

m < multiset.replicate (n + 1) x ↔ m ≤ multiset.replicate n x

source

def multiset.erase {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :

multiset α

erase s a is the multiset that subtracts 1 from the multiplicity of a.

Equations

s.erase a = quot.lift_on s (λ (l : list α), ↑(l.erase a)) _

source

@[simp]

theorem multiset.coe_erase {α : Type u_1} [decidable_eq α] (l : list α) (a : α) :

↑l.erase a = ↑(l.erase a)

source

@[simp]

theorem multiset.erase_zero {α : Type u_1} [decidable_eq α] (a : α) :

0.erase a = 0

source

@[simp]

theorem multiset.erase_cons_head {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

(a ::ₘ s).erase a = s

source

@[simp]

theorem multiset.erase_cons_tail {α : Type u_1} [decidable_eq α] {a b : α} (s : multiset α) (h : b ≠ a) :

(b ::ₘ s).erase a = b ::ₘ s.erase a

source

@[simp]

theorem multiset.erase_singleton {α : Type u_1} [decidable_eq α] (a : α) :

{a}.erase a = 0

source

@[simp]

theorem multiset.erase_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∉ s → s.erase a = s

source

@[simp]

theorem multiset.cons_erase {α : Type u_1} [decidable_eq α] {s : multiset α} {a : α} :

a ∈ s → a ::ₘ s.erase a = s

source

theorem multiset.le_cons_erase {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :

s ≤ a ::ₘ s.erase a

source

theorem multiset.add_singleton_eq_iff {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :

s + {a} = t ↔ a ∈ t ∧ s = t.erase a

source

theorem multiset.erase_add_left_pos {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (t : multiset α) :

a ∈ s → (s + t).erase a = s.erase a + t

source

theorem multiset.erase_add_right_pos {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} (h : a ∈ t) :

(s + t).erase a = s + t.erase a

source

theorem multiset.erase_add_right_neg {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (t : multiset α) :

a ∉ s → (s + t).erase a = s + t.erase a

source

theorem multiset.erase_add_left_neg {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} (h : a ∉ t) :

(s + t).erase a = s.erase a + t

source

theorem multiset.erase_le {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

s.erase a ≤ s

source

@[simp]

theorem multiset.erase_lt {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

s.erase a < s ↔ a ∈ s

source

theorem multiset.erase_subset {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

s.erase a ⊆ s

source

theorem multiset.mem_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} {s : multiset α} (ab : a ≠ b) :

a ∈ s.erase b ↔ a ∈ s

source

theorem multiset.mem_of_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : multiset α} :

a ∈ s.erase b → a ∈ s

source

theorem multiset.erase_comm {α : Type u_1} [decidable_eq α] (s : multiset α) (a b : α) :

(s.erase a).erase b = (s.erase b).erase a

source

theorem multiset.erase_le_erase {α : Type u_1} [decidable_eq α] {s t : multiset α} (a : α) (h : s ≤ t) :

s.erase a ≤ t.erase a

source

theorem multiset.erase_le_iff_le_cons {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :

s.erase a ≤ t ↔ s ≤ a ::ₘ t

source

@[simp]

theorem multiset.card_erase_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∈ s → ⇑multiset.card (s.erase a) = (⇑multiset.card s).pred

source

@[simp]

theorem multiset.card_erase_add_one {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∈ s → ⇑multiset.card (s.erase a) + 1 = ⇑multiset.card s

source

theorem multiset.card_erase_lt_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

a ∈ s → ⇑multiset.card (s.erase a) < ⇑multiset.card s

source

theorem multiset.card_erase_le {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

⇑multiset.card (s.erase a) ≤ ⇑multiset.card s

source

theorem multiset.card_erase_eq_ite {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

⇑multiset.card (s.erase a) = ite (a ∈ s) (⇑multiset.card s).pred (⇑multiset.card s)

source

@[simp]

theorem multiset.coe_reverse {α : Type u_1} (l : list α) :

↑(l.reverse) = ↑l

source

def multiset.map {α : Type u_1} {β : Type u_2} (f : α → β) (s : multiset α) :

multiset β

map f s is the lift of the list map operation. The multiplicity of b in map f s is the number of a ∈ s (counting multiplicity) such that f a = b.

Equations

multiset.map f s = quot.lift_on s (λ (l : list α), ↑(list.map f l)) _

Instances for multiset.map

multiset.can_lift

source

theorem multiset.map_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s t : multiset α} :

s = t → (∀ (x : α), x ∈ t → f x = g x) → multiset.map f s = multiset.map g t

source

theorem multiset.map_hcongr {α : Type u_1} {β β' : Type u_2} {m : multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀ (a : α), a ∈ m → f a == f' a) :

multiset.map f m == multiset.map f' m

source

theorem multiset.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Prop} {s : multiset α} :

(∀ (y : β), y ∈ multiset.map f s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)

source

@[simp]

theorem multiset.coe_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : list α) :

multiset.map f ↑l = ↑(list.map f l)

source

@[simp]

theorem multiset.map_zero {α : Type u_1} {β : Type u_2} (f : α → β) :

multiset.map f 0 = 0

source

@[simp]

theorem multiset.map_cons {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (s : multiset α) :

multiset.map f (a ::ₘ s) = f a ::ₘ multiset.map f s

source

theorem multiset.map_comp_cons {α : Type u_1} {β : Type u_2} (f : α → β) (t : α) :

multiset.map f ∘ multiset.cons t = multiset.cons (f t) ∘ multiset.map f

source

@[simp]

theorem multiset.map_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

multiset.map f {a} = {f a}

source

@[simp]

theorem multiset.map_replicate {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (k : ℕ) :

multiset.map f (multiset.replicate k a) = multiset.replicate k (f a)

source

@[simp]

theorem multiset.map_add {α : Type u_1} {β : Type u_2} (f : α → β) (s t : multiset α) :

multiset.map f (s + t) = multiset.map f s + multiset.map f t

source

@[protected, instance]

def multiset.can_lift {α : Type u_1} {β : Type u_2} (c : out_param (β → α)) (p : out_param (α → Prop)) [can_lift α β c p] :

can_lift (multiset α) (multiset β) (multiset.map c) (λ (s : multiset α), ∀ (x : α), x ∈ s → p x)

If each element of s : multiset α can be lifted to β, then s can be lifted to multiset β.

Equations

multiset.can_lift c p = {prf := _}

source

def multiset.map_add_monoid_hom {α : Type u_1} {β : Type u_2} (f : α → β) :

multiset α →+ multiset β

multiset.map as an add_monoid_hom.

Equations

multiset.map_add_monoid_hom f = {to_fun := multiset.map f, map_zero' := _, map_add' := _}

source

@[simp]

theorem multiset.coe_map_add_monoid_hom {α : Type u_1} {β : Type u_2} (f : α → β) :

⇑(multiset.map_add_monoid_hom f) = multiset.map f

source

theorem multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : multiset α) :

multiset.map f (n • s) = n • multiset.map f s

source

@[simp]

theorem multiset.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : multiset α} :

b ∈ multiset.map f s ↔ ∃ (a : α), a ∈ s ∧ f a = b

source

@[simp]

theorem multiset.card_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : multiset α) :

⇑multiset.card (multiset.map f s) = ⇑multiset.card s

source

@[simp]

theorem multiset.map_eq_zero {α : Type u_1} {β : Type u_2} {s : multiset α} {f : α → β} :

multiset.map f s = 0 ↔ s = 0

source

theorem multiset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α → β) {a : α} {s : multiset α} (h : a ∈ s) :

f a ∈ multiset.map f s

source

theorem multiset.map_eq_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {s : multiset α} {b : β} :

multiset.map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b

source

theorem multiset.map_eq_cons {α : Type u_1} {β : Type u_2} [decidable_eq α] (f : α → β) (s : multiset α) (t : multiset β) (b : β) :

(∃ (a : α) (H : a ∈ s), f a = b ∧ multiset.map f (s.erase a) = t) ↔ multiset.map f s = b ::ₘ t

source

theorem multiset.mem_map_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (H : function.injective f) {a : α} {s : multiset α} :

f a ∈ multiset.map f s ↔ a ∈ s

source

@[simp]

theorem multiset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (s : multiset α) :

multiset.map g (multiset.map f s) = multiset.map (g ∘ f) s

source

theorem multiset.map_id {α : Type u_1} (s : multiset α) :

multiset.map id s = s

source

@[simp]

theorem multiset.map_id' {α : Type u_1} (s : multiset α) :

multiset.map (λ (x : α), x) s = s

source

@[simp]

theorem multiset.map_const {α : Type u_1} {β : Type u_2} (s : multiset α) (b : β) :

multiset.map (function.const α b) s = multiset.replicate (⇑multiset.card s) b

source

theorem multiset.map_const' {α : Type u_1} {β : Type u_2} (s : multiset α) (b : β) :

multiset.map (λ (_x : α), b) s = multiset.replicate (⇑multiset.card s) b

source

theorem multiset.eq_of_mem_map_const {α : Type u_1} {β : Type u_2} {b₁ b₂ : β} {l : list α} (h : b₁ ∈ multiset.map (function.const α b₂) ↑l) :

b₁ = b₂

source

@[simp]

theorem multiset.map_le_map {α : Type u_1} {β : Type u_2} {f : α → β} {s t : multiset α} (h : s ≤ t) :

multiset.map f s ≤ multiset.map f t

source

@[simp]

theorem multiset.map_lt_map {α : Type u_1} {β : Type u_2} {f : α → β} {s t : multiset α} (h : s < t) :

multiset.map f s < multiset.map f t

source

theorem multiset.map_mono {α : Type u_1} {β : Type u_2} (f : α → β) :

monotone (multiset.map f)

source

theorem multiset.map_strict_mono {α : Type u_1} {β : Type u_2} (f : α → β) :

strict_mono (multiset.map f)

source

@[simp]

theorem multiset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α → β} {s t : multiset α} (H : s ⊆ t) :

multiset.map f s ⊆ multiset.map f t

source

theorem multiset.map_erase {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (hf : function.injective f) (x : α) (s : multiset α) :

multiset.map f (s.erase x) = (multiset.map f s).erase (f x)

source

theorem multiset.map_surjective_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) :

function.surjective (multiset.map f)

source

def multiset.foldl {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (s : multiset α) :

β

foldl f H b s is the lift of the list operation foldl f b l, which folds f over the multiset. It is well defined when f is right-commutative, that is, f (f b a₁) a₂ = f (f b a₂) a₁.

Equations

multiset.foldl f H b s = quot.lift_on s (λ (l : list α), list.foldl f b l) _

source

@[simp]

theorem multiset.foldl_zero {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) :

multiset.foldl f H b 0 = b

source

@[simp]

theorem multiset.foldl_cons {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (a : α) (s : multiset α) :

multiset.foldl f H b (a ::ₘ s) = multiset.foldl f H (f b a) s

source

@[simp]

theorem multiset.foldl_add {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (s t : multiset α) :

multiset.foldl f H b (s + t) = multiset.foldl f H (multiset.foldl f H b s) t

source

def multiset.foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (s : multiset α) :

β

foldr f H b s is the lift of the list operation foldr f b l, which folds f over the multiset. It is well defined when f is left-commutative, that is, f a₁ (f a₂ b) = f a₂ (f a₁ b).

Equations

multiset.foldr f H b s = quot.lift_on s (λ (l : list α), list.foldr f b l) _

source

@[simp]

theorem multiset.foldr_zero {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) :

multiset.foldr f H b 0 = b

source

@[simp]

theorem multiset.foldr_cons {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (a : α) (s : multiset α) :

multiset.foldr f H b (a ::ₘ s) = f a (multiset.foldr f H b s)

source

@[simp]

theorem multiset.foldr_singleton {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (a : α) :

multiset.foldr f H b {a} = f a b

source

@[simp]

theorem multiset.foldr_add {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (s t : multiset α) :

multiset.foldr f H b (s + t) = multiset.foldr f H (multiset.foldr f H b t) s

source

@[simp]

theorem multiset.coe_foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (l : list α) :

multiset.foldr f H b ↑l = list.foldr f b l

source

@[simp]

theorem multiset.coe_foldl {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (l : list α) :

multiset.foldl f H b ↑l = list.foldl f b l

source

theorem multiset.coe_foldr_swap {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (l : list α) :

multiset.foldr f H b ↑l = list.foldl (λ (x : β) (y : α), f y x) b l

source

theorem multiset.foldr_swap {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (s : multiset α) :

multiset.foldr f H b s = multiset.foldl (λ (x : β) (y : α), f y x) _ b s

source

theorem multiset.foldl_swap {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (s : multiset α) :

multiset.foldl f H b s = multiset.foldr (λ (x : α) (y : β), f y x) _ b s

source

theorem multiset.foldr_induction' {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (x : β) (q : α → Prop) (p : β → Prop) (s : multiset α) (hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)) (px : p x) (q_s : ∀ (a : α), a ∈ s → q a) :

p (multiset.foldr f H x s)

source

theorem multiset.foldr_induction {α : Type u_1} (f : α → α → α) (H : left_commutative f) (x : α) (p : α → Prop) (s : multiset α) (p_f : ∀ (a b : α), p a → p b → p (f a b)) (px : p x) (p_s : ∀ (a : α), a ∈ s → p a) :

p (multiset.foldr f H x s)

source

theorem multiset.foldl_induction' {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (x : β) (q : α → Prop) (p : β → Prop) (s : multiset α) (hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)) (px : p x) (q_s : ∀ (a : α), a ∈ s → q a) :

p (multiset.foldl f H x s)

source

theorem multiset.foldl_induction {α : Type u_1} (f : α → α → α) (H : right_commutative f) (x : α) (p : α → Prop) (s : multiset α) (p_f : ∀ (a b : α), p a → p b → p (f b a)) (px : p x) (p_s : ∀ (a : α), a ∈ s → p a) :

p (multiset.foldl f H x s)

source

def multiset.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (s : multiset α) :

(∀ (a : α), a ∈ s → p a) → multiset β

Lift of the list pmap operation. Map a partial function f over a multiset s whose elements are all in the domain of f.

Equations

multiset.pmap f s = quot.rec_on s (λ (l : list α) (H : ∀ (a : α), a ∈ quot.mk setoid.r l → p a), ↑(list.pmap f l H)) _

source

@[simp]

theorem multiset.coe_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (l : list α) (H : ∀ (a : α), a ∈ l → p a) :

multiset.pmap f ↑l H = ↑(list.pmap f l H)

source

@[simp]

theorem multiset.pmap_zero {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (h : ∀ (a : α), a ∈ 0 → p a) :

multiset.pmap f 0 h = 0

source

@[simp]

theorem multiset.pmap_cons {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (a : α) (m : multiset α) (h : ∀ (b : α), b ∈ a ::ₘ m → p b) :

multiset.pmap f (a ::ₘ m) h = f a _ ::ₘ multiset.pmap f m _

source

def multiset.attach {α : Type u_1} (s : multiset α) :

multiset {x // x ∈ s}

"Attach" a proof that a ∈ s to each element a in s to produce a multiset on {x // x ∈ s}.

Equations

s.attach = multiset.pmap subtype.mk s _

source

@[simp]

theorem multiset.coe_attach {α : Type u_1} (l : list α) :

↑l.attach = ↑(l.attach)

source

theorem multiset.sizeof_lt_sizeof_of_mem {α : Type u_1} [has_sizeof α] {x : α} {s : multiset α} (hx : x ∈ s) :

sizeof x < sizeof s

source

theorem multiset.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (s : multiset α) (H : ∀ (a : α), a ∈ s → p a) :

multiset.pmap (λ (a : α) (_x : p a), f a) s H = multiset.map f s

source

theorem multiset.pmap_congr {α : Type u_1} {β : Type u_2} {p q : α → Prop} {f : Π (a : α), p a → β} {g : Π (a : α), q a → β} (s : multiset α) {H₁ : ∀ (a : α), a ∈ s → p a} {H₂ : ∀ (a : α), a ∈ s → q a} :

(∀ (a : α), a ∈ s → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → multiset.pmap f s H₁ = multiset.pmap g s H₂

source

theorem multiset.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : Π (a : α), p a → β) (s : multiset α) (H : ∀ (a : α), a ∈ s → p a) :

multiset.map g (multiset.pmap f s H) = multiset.pmap (λ (a : α) (h : p a), g (f a h)) s H

source

theorem multiset.pmap_eq_map_attach {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (s : multiset α) (H : ∀ (a : α), a ∈ s → p a) :

multiset.pmap f s H = multiset.map (λ (x : {x // x ∈ s}), f ↑x _) s.attach

source

@[simp]

theorem multiset.attach_map_coe' {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → β) :

multiset.map (λ (i : {x // x ∈ s}), f ↑i) s.attach = multiset.map f s

source

theorem multiset.attach_map_val' {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → β) :

multiset.map (λ (i : {x // x ∈ s}), f i.val) s.attach = multiset.map f s

source

@[simp]

theorem multiset.attach_map_coe {α : Type u_1} (s : multiset α) :

multiset.map coe s.attach = s

source

theorem multiset.attach_map_val {α : Type u_1} (s : multiset α) :

multiset.map subtype.val s.attach = s

source

@[simp]

theorem multiset.mem_attach {α : Type u_1} (s : multiset α) (x : {x // x ∈ s}) :

x ∈ s.attach

source

@[simp]

theorem multiset.mem_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : Π (a : α), p a → β} {s : multiset α} {H : ∀ (a : α), a ∈ s → p a} {b : β} :

b ∈ multiset.pmap f s H ↔ ∃ (a : α) (h : a ∈ s), f a _ = b

source

@[simp]

theorem multiset.card_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (s : multiset α) (H : ∀ (a : α), a ∈ s → p a) :

⇑multiset.card (multiset.pmap f s H) = ⇑multiset.card s

source

@[simp]

theorem multiset.card_attach {α : Type u_1} {m : multiset α} :

⇑multiset.card m.attach = ⇑multiset.card m

source

@[simp]

theorem multiset.attach_zero {α : Type u_1} :

0.attach = 0

source

theorem multiset.attach_cons {α : Type u_1} (a : α) (m : multiset α) :

(a ::ₘ m).attach = ⟨a, _⟩ ::ₘ multiset.map (λ (p : {x // x ∈ m}), ⟨p.val, _⟩) m.attach

source

@[protected]

def multiset.decidable_forall_multiset {α : Type u_1} {m : multiset α} {p : α → Prop} [hp : Π (a : α), decidable (p a)] :

decidable (∀ (a : α), a ∈ m → p a)

If p is a decidable predicate, so is the predicate that all elements of a multiset satisfy p.

Equations

multiset.decidable_forall_multiset = quotient.rec_on_subsingleton m (λ (l : list α), decidable_of_iff (∀ (a : α), a ∈ l → p a) _)

source

@[protected, instance]

def multiset.decidable_dforall_multiset {α : Type u_1} {m : multiset α} {p : Π (a : α), a ∈ m → Prop} [hp : Π (a : α) (h : a ∈ m), decidable (p a h)] :

decidable (∀ (a : α) (h : a ∈ m), p a h)

Equations

multiset.decidable_dforall_multiset = decidable_of_decidable_of_iff multiset.decidable_forall_multiset multiset.decidable_dforall_multiset._proof_3

source

@[protected, instance]

def multiset.decidable_eq_pi_multiset {α : Type u_1} {m : multiset α} {β : α → Type u_2} [h : Π (a : α), decidable_eq (β a)] :

decidable_eq (Π (a : α), a ∈ m → β a)

decidable equality for functions whose domain is bounded by multisets

Equations

multiset.decidable_eq_pi_multiset = λ (f g : Π (a : α), a ∈ m → β a), decidable_of_iff (∀ (a : α) (h : a ∈ m), f a h = g a h) _

source

@[protected]

def multiset.decidable_exists_multiset {α : Type u_1} {m : multiset α} {p : α → Prop} [decidable_pred p] :

decidable (∃ (x : α) (H : x ∈ m), p x)

If p is a decidable predicate, so is the existence of an element in a multiset satisfying p.

Equations

multiset.decidable_exists_multiset = quotient.rec_on_subsingleton m (λ (l : list α), decidable_of_iff (∃ (a : α) (H : a ∈ l), p a) _)

source

@[protected, instance]

def multiset.decidable_dexists_multiset {α : Type u_1} {m : multiset α} {p : Π (a : α), a ∈ m → Prop} [hp : Π (a : α) (h : a ∈ m), decidable (p a h)] :

decidable (∃ (a : α) (h : a ∈ m), p a h)

Equations

multiset.decidable_dexists_multiset = decidable_of_decidable_of_iff multiset.decidable_exists_multiset multiset.decidable_dexists_multiset._proof_3

source

@[protected]

def multiset.sub {α : Type u_1} [decidable_eq α] (s t : multiset α) :

multiset α

s - t is the multiset such that count a (s - t) = count a s - count a t for all a (note that it is truncated subtraction, so it is 0 if count a t ≥ count a s).

Equations

s.sub t = quotient.lift_on₂ s t (λ (l₁ l₂ : list α), ↑(l₁.diff l₂)) multiset.sub._proof_1

source

@[protected, instance]

def multiset.has_sub {α : Type u_1} [decidable_eq α] :

has_sub (multiset α)

Equations

multiset.has_sub = {sub := multiset.sub (λ (a b : α), _inst_1 a b)}

source

@[simp]

theorem multiset.coe_sub {α : Type u_1} [decidable_eq α] (s t : list α) :

↑s - ↑t = ↑(s.diff t)

source

@[protected]

theorem multiset.sub_zero {α : Type u_1} [decidable_eq α] (s : multiset α) :

s - 0 = s

This is a special case of tsub_zero, which should be used instead of this. This is needed to prove has_ordered_sub (multiset α).

source

@[simp]

theorem multiset.sub_cons {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

s - a ::ₘ t = s.erase a - t

source

@[protected]

theorem multiset.sub_le_iff_le_add {α : Type u_1} [decidable_eq α] {s t u : multiset α} :

s - t ≤ u ↔ s ≤ u + t

This is a special case of tsub_le_iff_right, which should be used instead of this. This is needed to prove has_ordered_sub (multiset α).

source

@[protected, instance]

def multiset.has_ordered_sub {α : Type u_1} [decidable_eq α] :

has_ordered_sub (multiset α)

source

theorem multiset.cons_sub_of_le {α : Type u_1} [decidable_eq α] (a : α) {s t : multiset α} (h : t ≤ s) :

a ::ₘ s - t = a ::ₘ (s - t)

source

theorem multiset.sub_eq_fold_erase {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s - t = multiset.foldl multiset.erase multiset.erase_comm s t

source

@[simp]

theorem multiset.card_sub {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : t ≤ s) :

⇑multiset.card (s - t) = ⇑multiset.card s - ⇑multiset.card t

source

def multiset.union {α : Type u_1} [decidable_eq α] (s t : multiset α) :

multiset α

s ∪ t is the lattice join operation with respect to the multiset ≤. The multiplicity of a in s ∪ t is the maximum of the multiplicities in s and t.

Equations

s.union t = s - t + t

source

@[protected, instance]

def multiset.has_union {α : Type u_1} [decidable_eq α] :

has_union (multiset α)

Equations

multiset.has_union = {union := multiset.union (λ (a b : α), _inst_1 a b)}

source

theorem multiset.union_def {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∪ t = s - t + t

source

theorem multiset.le_union_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ≤ s ∪ t

source

theorem multiset.le_union_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :

t ≤ s ∪ t

source

theorem multiset.eq_union_left {α : Type u_1} [decidable_eq α] {s t : multiset α} :

t ≤ s → s ∪ t = s

source

theorem multiset.union_le_union_right {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s ≤ t) (u : multiset α) :

s ∪ u ≤ t ∪ u

source

theorem multiset.union_le {α : Type u_1} [decidable_eq α] {s t u : multiset α} (h₁ : s ≤ u) (h₂ : t ≤ u) :

s ∪ t ≤ u

source

@[simp]

theorem multiset.mem_union {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :

a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

source

@[simp]

theorem multiset.map_union {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {s t : multiset α} :

multiset.map f (s ∪ t) = multiset.map f s ∪ multiset.map f t

source

def multiset.inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :

multiset α

s ∩ t is the lattice meet operation with respect to the multiset ≤. The multiplicity of a in s ∩ t is the minimum of the multiplicities in s and t.

Equations

s.inter t = quotient.lift_on₂ s t (λ (l₁ l₂ : list α), ↑(l₁.bag_inter l₂)) multiset.inter._proof_1

source

@[protected, instance]

def multiset.has_inter {α : Type u_1} [decidable_eq α] :

has_inter (multiset α)

Equations

multiset.has_inter = {inter := multiset.inter (λ (a b : α), _inst_1 a b)}

source

@[simp]

theorem multiset.inter_zero {α : Type u_1} [decidable_eq α] (s : multiset α) :

s ∩ 0 = 0

source

@[simp]

theorem multiset.zero_inter {α : Type u_1} [decidable_eq α] (s : multiset α) :

0 ∩ s = 0

source

@[simp]

theorem multiset.cons_inter_of_pos {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} :

a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a

source

@[simp]

theorem multiset.cons_inter_of_neg {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} :

a ∉ t → (a ::ₘ s) ∩ t = s ∩ t

source

theorem multiset.inter_le_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∩ t ≤ s

source

theorem multiset.inter_le_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∩ t ≤ t

source

theorem multiset.le_inter {α : Type u_1} [decidable_eq α] {s t u : multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u) :

s ≤ t ∩ u

source

@[simp]

theorem multiset.mem_inter {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :

a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t

source

@[protected, instance]

def multiset.lattice {α : Type u_1} [decidable_eq α] :

lattice (multiset α)

Equations

multiset.lattice = {sup := has_union.union multiset.has_union, le := partial_order.le multiset.partial_order, lt := partial_order.lt multiset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter multiset.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[simp]

theorem multiset.sup_eq_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ⊔ t = s ∪ t

source

@[simp]

theorem multiset.inf_eq_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ⊓ t = s ∩ t

source

@[simp]

theorem multiset.le_inter_iff {α : Type u_1} [decidable_eq α] {s t u : multiset α} :

s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u

source

@[simp]

theorem multiset.union_le_iff {α : Type u_1} [decidable_eq α] {s t u : multiset α} :

s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u

source

theorem multiset.union_comm {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∪ t = t ∪ s

source

theorem multiset.inter_comm {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∩ t = t ∩ s

source

theorem multiset.eq_union_right {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s ≤ t) :

s ∪ t = t

source

theorem multiset.union_le_union_left {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s ≤ t) (u : multiset α) :

u ∪ s ≤ u ∪ t

source

theorem multiset.union_le_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∪ t ≤ s + t

source

theorem multiset.union_add_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :

s ∪ t + u = s + u ∪ (t + u)

source

theorem multiset.add_union_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :

s + (t ∪ u) = s + t ∪ (s + u)

source

theorem multiset.cons_union_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

source

theorem multiset.inter_add_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :

s ∩ t + u = (s + u) ∩ (t + u)

source

theorem multiset.add_inter_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :

s + t ∩ u = (s + t) ∩ (s + u)

source

theorem multiset.cons_inter_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

source

theorem multiset.union_add_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s ∪ t + s ∩ t = s + t

source

theorem multiset.sub_add_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s - t + s ∩ t = s

source

theorem multiset.sub_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :

s - s ∩ t = s - t

source

def multiset.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset α

filter p s returns the elements in s (with the same multiplicities) which satisfy p, and removes the rest.

Equations

multiset.filter p s = quot.lift_on s (λ (l : list α), ↑(list.filter p l)) _

source

@[simp]

theorem multiset.coe_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

multiset.filter p ↑l = ↑(list.filter p l)

source

@[simp]

theorem multiset.filter_zero {α : Type u_1} (p : α → Prop) [decidable_pred p] :

multiset.filter p 0 = 0

source

theorem multiset.filter_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {s : multiset α} :

(∀ (x : α), x ∈ s → (p x ↔ q x)) → multiset.filter p s = multiset.filter q s

source

@[simp]

theorem multiset.filter_add {α : Type u_1} (p : α → Prop) [decidable_pred p] (s t : multiset α) :

multiset.filter p (s + t) = multiset.filter p s + multiset.filter p t

source

@[simp]

theorem multiset.filter_le {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset.filter p s ≤ s

source

@[simp]

theorem multiset.filter_subset {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset.filter p s ⊆ s

source

theorem multiset.filter_le_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] {s t : multiset α} (h : s ≤ t) :

multiset.filter p s ≤ multiset.filter p t

source

theorem multiset.monotone_filter_left {α : Type u_1} (p : α → Prop) [decidable_pred p] :

monotone (multiset.filter p)

source

theorem multiset.monotone_filter_right {α : Type u_1} (s : multiset α) ⦃p q : α → Prop⦄ [decidable_pred p] [decidable_pred q] (h : p ≤ q) :

multiset.filter p s ≤ multiset.filter q s

source

@[simp]

theorem multiset.filter_cons_of_pos {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

p a → multiset.filter p (a ::ₘ s) = a ::ₘ multiset.filter p s

source

@[simp]

theorem multiset.filter_cons_of_neg {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

¬p a → multiset.filter p (a ::ₘ s) = multiset.filter p s

source

@[simp]

theorem multiset.mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :

a ∈ multiset.filter p s ↔ a ∈ s ∧ p a

source

theorem multiset.of_mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} (h : a ∈ multiset.filter p s) :

p a

source

theorem multiset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} (h : a ∈ multiset.filter p s) :

a ∈ s

source

theorem multiset.mem_filter_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {l : multiset α} (m : a ∈ l) (h : p a) :

a ∈ multiset.filter p l

source

theorem multiset.filter_eq_self {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :

multiset.filter p s = s ↔ ∀ (a : α), a ∈ s → p a

source

theorem multiset.filter_eq_nil {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :

multiset.filter p s = 0 ↔ ∀ (a : α), a ∈ s → ¬p a

source

theorem multiset.le_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s t : multiset α} :

s ≤ multiset.filter p t ↔ s ≤ t ∧ ∀ (a : α), a ∈ s → p a

source

theorem multiset.filter_cons {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

multiset.filter p (a ::ₘ s) = ite (p a) {a} 0 + multiset.filter p s

source

theorem multiset.filter_singleton {α : Type u_1} {a : α} (p : α → Prop) [decidable_pred p] :

multiset.filter p {a} = ite (p a) {a} ∅

source

theorem multiset.filter_nsmul {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : multiset α) (n : ℕ) :

multiset.filter p (n • s) = n • multiset.filter p s

source

@[simp]

theorem multiset.filter_sub {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s t : multiset α) :

multiset.filter p (s - t) = multiset.filter p s - multiset.filter p t

source

@[simp]

theorem multiset.filter_union {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s t : multiset α) :

multiset.filter p (s ∪ t) = multiset.filter p s ∪ multiset.filter p t

source

@[simp]

theorem multiset.filter_inter {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s t : multiset α) :

multiset.filter p (s ∩ t) = multiset.filter p s ∩ multiset.filter p t

source

@[simp]

theorem multiset.filter_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (q : α → Prop) [decidable_pred q] (s : multiset α) :

multiset.filter p (multiset.filter q s) = multiset.filter (λ (a : α), p a ∧ q a) s

source

theorem multiset.filter_comm {α : Type u_1} (p : α → Prop) [decidable_pred p] (q : α → Prop) [decidable_pred q] (s : multiset α) :

multiset.filter p (multiset.filter q s) = multiset.filter q (multiset.filter p s)

source

theorem multiset.filter_add_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (q : α → Prop) [decidable_pred q] (s : multiset α) :

multiset.filter p s + multiset.filter q s = multiset.filter (λ (a : α), p a ∨ q a) s + multiset.filter (λ (a : α), p a ∧ q a) s

source

theorem multiset.filter_add_not {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset.filter p s + multiset.filter (λ (a : α), ¬p a) s = s

source

theorem multiset.map_filter {α : Type u_1} {β : Type u_2} (p : α → Prop) [decidable_pred p] (f : β → α) (s : multiset β) :

multiset.filter p (multiset.map f s) = multiset.map f (multiset.filter (p ∘ f) s)

source

theorem multiset.map_filter' {α : Type u_1} {β : Type u_2} (p : α → Prop) [decidable_pred p] {f : α → β} (hf : function.injective f) (s : multiset α) [decidable_pred (λ (b : β), ∃ (a : α), p a ∧ f a = b)] :

multiset.map f (multiset.filter p s) = multiset.filter (λ (b : β), ∃ (a : α), p a ∧ f a = b) (multiset.map f s)

source

def multiset.filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (s : multiset α) :

multiset β

filter_map f s is a combination filter/map operation on s. The function f : α → option β is applied to each element of s; if f a is some b then b is added to the result, otherwise a is removed from the resulting multiset.

Equations

multiset.filter_map f s = quot.lift_on s (λ (l : list α), ↑(list.filter_map f l)) _

source

@[simp]

theorem multiset.coe_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (l : list α) :

multiset.filter_map f ↑l = ↑(list.filter_map f l)

source

@[simp]

theorem multiset.filter_map_zero {α : Type u_1} {β : Type u_2} (f : α → option β) :

multiset.filter_map f 0 = 0

source

@[simp]

theorem multiset.filter_map_cons_none {α : Type u_1} {β : Type u_2} {f : α → option β} (a : α) (s : multiset α) (h : f a = option.none) :

multiset.filter_map f (a ::ₘ s) = multiset.filter_map f s

source

@[simp]

theorem multiset.filter_map_cons_some {α : Type u_1} {β : Type u_2} (f : α → option β) (a : α) (s : multiset α) {b : β} (h : f a = option.some b) :

multiset.filter_map f (a ::ₘ s) = b ::ₘ multiset.filter_map f s

source

theorem multiset.filter_map_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) :

multiset.filter_map (option.some ∘ f) = multiset.map f

source

theorem multiset.filter_map_eq_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] :

multiset.filter_map (option.guard p) = multiset.filter p

source

theorem multiset.filter_map_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → option β) (g : β → option γ) (s : multiset α) :

multiset.filter_map g (multiset.filter_map f s) = multiset.filter_map (λ (x : α), (f x).bind g) s

source

theorem multiset.map_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → option β) (g : β → γ) (s : multiset α) :

multiset.map g (multiset.filter_map f s) = multiset.filter_map (λ (x : α), option.map g (f x)) s

source

theorem multiset.filter_map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → option γ) (s : multiset α) :

multiset.filter_map g (multiset.map f s) = multiset.filter_map (g ∘ f) s

source

theorem multiset.filter_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (p : β → Prop) [decidable_pred p] (s : multiset α) :

multiset.filter p (multiset.filter_map f s) = multiset.filter_map (λ (x : α), option.filter p (f x)) s

source

theorem multiset.filter_map_filter {α : Type u_1} {β : Type u_2} (p : α → Prop) [decidable_pred p] (f : α → option β) (s : multiset α) :

multiset.filter_map f (multiset.filter p s) = multiset.filter_map (λ (x : α), ite (p x) (f x) option.none) s

source

@[simp]

theorem multiset.filter_map_some {α : Type u_1} (s : multiset α) :

multiset.filter_map option.some s = s

source

@[simp]

theorem multiset.mem_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (s : multiset α) {b : β} :

b ∈ multiset.filter_map f s ↔ ∃ (a : α), a ∈ s ∧ f a = option.some b

source

theorem multiset.map_filter_map_of_inv {α : Type u_1} {β : Type u_2} (f : α → option β) (g : β → α) (H : ∀ (x : α), option.map g (f x) = option.some x) (s : multiset α) :

multiset.map g (multiset.filter_map f s) = s

source

theorem multiset.filter_map_le_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) {s t : multiset α} (h : s ≤ t) :

multiset.filter_map f s ≤ multiset.filter_map f t

source

def multiset.countp {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

ℕ

countp p s counts the number of elements of s (with multiplicity) that satisfy p.

Equations

multiset.countp p s = quot.lift_on s (list.countp p) _

source

@[simp]

theorem multiset.coe_countp {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

multiset.countp p ↑l = list.countp p l

source

@[simp]

theorem multiset.countp_zero {α : Type u_1} (p : α → Prop) [decidable_pred p] :

multiset.countp p 0 = 0

source

@[simp]

theorem multiset.countp_cons_of_pos {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

p a → multiset.countp p (a ::ₘ s) = multiset.countp p s + 1

source

@[simp]

theorem multiset.countp_cons_of_neg {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

¬p a → multiset.countp p (a ::ₘ s) = multiset.countp p s

source

theorem multiset.countp_cons {α : Type u_1} (p : α → Prop) [decidable_pred p] (b : α) (s : multiset α) :

multiset.countp p (b ::ₘ s) = multiset.countp p s + ite (p b) 1 0

source

theorem multiset.countp_eq_card_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset.countp p s = ⇑multiset.card (multiset.filter p s)

source

theorem multiset.countp_le_card {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset.countp p s ≤ ⇑multiset.card s

source

@[simp]

theorem multiset.countp_add {α : Type u_1} (p : α → Prop) [decidable_pred p] (s t : multiset α) :

multiset.countp p (s + t) = multiset.countp p s + multiset.countp p t

source

@[simp]

theorem multiset.countp_nsmul {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) (n : ℕ) :

multiset.countp p (n • s) = n * multiset.countp p s

source

theorem multiset.card_eq_countp_add_countp {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

⇑multiset.card s = multiset.countp p s + multiset.countp (λ (x : α), ¬p x) s

source

def multiset.countp_add_monoid_hom {α : Type u_1} (p : α → Prop) [decidable_pred p] :

multiset α →+ ℕ

countp p, the number of elements of a multiset satisfying p, promoted to an add_monoid_hom.

Equations

multiset.countp_add_monoid_hom p = {to_fun := multiset.countp p (λ (a : α), _inst_1 a), map_zero' := _, map_add' := _}

source

@[simp]

theorem multiset.coe_countp_add_monoid_hom {α : Type u_1} (p : α → Prop) [decidable_pred p] :

⇑(multiset.countp_add_monoid_hom p) = multiset.countp p

source

@[simp]

theorem multiset.countp_sub {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] {s t : multiset α} (h : t ≤ s) :

multiset.countp p (s - t) = multiset.countp p s - multiset.countp p t

source

theorem multiset.countp_le_of_le {α : Type u_1} (p : α → Prop) [decidable_pred p] {s t : multiset α} (h : s ≤ t) :

multiset.countp p s ≤ multiset.countp p t

source

@[simp]

theorem multiset.countp_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (q : α → Prop) [decidable_pred q] (s : multiset α) :

multiset.countp p (multiset.filter q s) = multiset.countp (λ (a : α), p a ∧ q a) s

source

theorem multiset.countp_eq_countp_filter_add {α : Type u_1} (s : multiset α) (p q : α → Prop) [decidable_pred p] [decidable_pred q] :

multiset.countp p s = multiset.countp p (multiset.filter q s) + multiset.countp p (multiset.filter (λ (a : α), ¬q a) s)

source

@[simp]

theorem multiset.countp_true {α : Type u_1} {s : multiset α} :

multiset.countp (λ (_x : α), true) s = ⇑multiset.card s

source

@[simp]

theorem multiset.countp_false {α : Type u_1} {s : multiset α} :

multiset.countp (λ (_x : α), false) s = 0

source

theorem multiset.countp_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : multiset α) (p : β → Prop) [decidable_pred p] :

multiset.countp p (multiset.map f s) = ⇑multiset.card (multiset.filter (λ (a : α), p (f a)) s)

source

@[simp]

theorem multiset.countp_attach {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : multiset α) :

multiset.countp (λ (a : {x // x ∈ s}), p ↑a) s.attach = multiset.countp p s

source

@[simp]

theorem multiset.filter_attach {α : Type u_1} (m : multiset α) (p : α → Prop) [decidable_pred p] :

multiset.filter (λ (x : {x // x ∈ m}), p ↑x) m.attach = multiset.map (subtype.map id _) (multiset.filter p m).attach

source

theorem multiset.countp_pos {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :

0 < multiset.countp p s ↔ ∃ (a : α) (H : a ∈ s), p a

source

theorem multiset.countp_eq_zero {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :

multiset.countp p s = 0 ↔ ∀ (a : α), a ∈ s → ¬p a

source

theorem multiset.countp_eq_card {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :

multiset.countp p s = ⇑multiset.card s ↔ ∀ (a : α), a ∈ s → p a

source

theorem multiset.countp_pos_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} {a : α} (h : a ∈ s) (pa : p a) :

0 < multiset.countp p s

source

theorem multiset.countp_congr {α : Type u_1} {s s' : multiset α} (hs : s = s') {p p' : α → Prop} [decidable_pred p] [decidable_pred p'] (hp : ∀ (x : α), x ∈ s → (p x ↔ p' x)) :

multiset.countp p s = multiset.countp p' s'

source

def multiset.count {α : Type u_1} [decidable_eq α] (a : α) :

multiset α → ℕ

count a s is the multiplicity of a in s.

Equations

multiset.count a = multiset.countp (eq a)

source

@[simp]

theorem multiset.coe_count {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :

multiset.count a ↑l = list.count a l

source

@[simp]

theorem multiset.count_zero {α : Type u_1} [decidable_eq α] (a : α) :

multiset.count a 0 = 0

source

@[simp]

theorem multiset.count_cons_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

multiset.count a (a ::ₘ s) = (multiset.count a s).succ

source

@[simp]

theorem multiset.count_cons_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (h : a ≠ b) (s : multiset α) :

multiset.count a (b ::ₘ s) = multiset.count a s

source

theorem multiset.count_le_card {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

multiset.count a s ≤ ⇑multiset.card s

source

theorem multiset.count_le_of_le {α : Type u_1} [decidable_eq α] (a : α) {s t : multiset α} :

s ≤ t → multiset.count a s ≤ multiset.count a t

source

theorem multiset.count_le_count_cons {α : Type u_1} [decidable_eq α] (a b : α) (s : multiset α) :

multiset.count a s ≤ multiset.count a (b ::ₘ s)

source

theorem multiset.count_cons {α : Type u_1} [decidable_eq α] (a b : α) (s : multiset α) :

multiset.count a (b ::ₘ s) = multiset.count a s + ite (a = b) 1 0

source

theorem multiset.count_singleton_self {α : Type u_1} [decidable_eq α] (a : α) :

multiset.count a {a} = 1

source

theorem multiset.count_singleton {α : Type u_1} [decidable_eq α] (a b : α) :

multiset.count a {b} = ite (a = b) 1 0

source

@[simp]

theorem multiset.count_add {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

multiset.count a (s + t) = multiset.count a s + multiset.count a t

source

def multiset.count_add_monoid_hom {α : Type u_1} [decidable_eq α] (a : α) :

multiset α →+ ℕ

count a, the multiplicity of a in a multiset, promoted to an add_monoid_hom.

Equations

multiset.count_add_monoid_hom a = multiset.countp_add_monoid_hom (eq a)

source

@[simp]

theorem multiset.coe_count_add_monoid_hom {α : Type u_1} [decidable_eq α] {a : α} :

⇑(multiset.count_add_monoid_hom a) = multiset.count a

source

@[simp]

theorem multiset.count_nsmul {α : Type u_1} [decidable_eq α] (a : α) (n : ℕ) (s : multiset α) :

multiset.count a (n • s) = n * multiset.count a s

source

@[simp]

theorem multiset.count_attach {α : Type u_1} [decidable_eq α] {s : multiset α} (a : {x // x ∈ s}) :

multiset.count a s.attach = multiset.count ↑a s

source

theorem multiset.count_pos {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

0 < multiset.count a s ↔ a ∈ s

source

theorem multiset.one_le_count_iff_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

1 ≤ multiset.count a s ↔ a ∈ s

source

@[simp]

theorem multiset.count_eq_zero_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (h : a ∉ s) :

multiset.count a s = 0

source

@[simp]

theorem multiset.count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

multiset.count a s = 0 ↔ a ∉ s

source

theorem multiset.count_ne_zero {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

multiset.count a s ≠ 0 ↔ a ∈ s

source

theorem multiset.count_eq_card {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

multiset.count a s = ⇑multiset.card s ↔ ∀ (x : α), x ∈ s → a = x

source

@[simp]

theorem multiset.count_replicate_self {α : Type u_1} [decidable_eq α] (a : α) (n : ℕ) :

multiset.count a (multiset.replicate n a) = n

source

theorem multiset.count_replicate {α : Type u_1} [decidable_eq α] (a b : α) (n : ℕ) :

multiset.count a (multiset.replicate n b) = ite (a = b) n 0

source

@[simp]

theorem multiset.count_erase_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

multiset.count a (s.erase a) = (multiset.count a s).pred

source

@[simp]

theorem multiset.count_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (ab : a ≠ b) (s : multiset α) :

multiset.count a (s.erase b) = multiset.count a s

source

@[simp]

theorem multiset.count_sub {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

multiset.count a (s - t) = multiset.count a s - multiset.count a t

source

@[simp]

theorem multiset.count_union {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

multiset.count a (s ∪ t) = linear_order.max (multiset.count a s) (multiset.count a t)

source

@[simp]

theorem multiset.count_inter {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

multiset.count a (s ∩ t) = linear_order.min (multiset.count a s) (multiset.count a t)

source

theorem multiset.le_count_iff_replicate_le {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} {n : ℕ} :

n ≤ multiset.count a s ↔ multiset.replicate n a ≤ s

source

@[simp]

theorem multiset.count_filter_of_pos {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} (h : p a) :

multiset.count a (multiset.filter p s) = multiset.count a s

source

@[simp]

theorem multiset.count_filter_of_neg {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} (h : ¬p a) :

multiset.count a (multiset.filter p s) = 0

source

theorem multiset.count_filter {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :

multiset.count a (multiset.filter p s) = ite (p a) (multiset.count a s) 0

source

theorem multiset.ext {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s = t ↔ ∀ (a : α), multiset.count a s = multiset.count a t

source

@[ext]

theorem multiset.ext' {α : Type u_1} [decidable_eq α] {s t : multiset α} :

(∀ (a : α), multiset.count a s = multiset.count a t) → s = t

source

@[simp]

theorem multiset.coe_inter {α : Type u_1} [decidable_eq α] (s t : list α) :

↑s ∩ ↑t = ↑(s.bag_inter t)

source

theorem multiset.le_iff_count {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s ≤ t ↔ ∀ (a : α), multiset.count a s ≤ multiset.count a t

source

@[protected, instance]

def multiset.distrib_lattice {α : Type u_1} [decidable_eq α] :

distrib_lattice (multiset α)

Equations

multiset.distrib_lattice = {sup := lattice.sup multiset.lattice, le := lattice.le multiset.lattice, lt := lattice.lt multiset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf multiset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

theorem multiset.count_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : multiset α) [decidable_eq β] (b : β) :

multiset.count b (multiset.map f s) = ⇑multiset.card (multiset.filter (λ (a : α), b = f a) s)

source

theorem multiset.count_map_eq_count {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (s : multiset α) (hf : set.inj_on f {x : α | x ∈ s}) (x : α) (H : x ∈ s) :

multiset.count (f x) (multiset.map f s) = multiset.count x s

multiset.map f preserves count if f is injective on the set of elements contained in the multiset

source

theorem multiset.count_map_eq_count' {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (s : multiset α) (hf : function.injective f) (x : α) :

multiset.count (f x) (multiset.map f s) = multiset.count x s

multiset.map f preserves count if f is injective

source

theorem multiset.filter_eq' {α : Type u_1} [decidable_eq α] (s : multiset α) (b : α) :

multiset.filter (λ (_x : α), _x = b) s = multiset.replicate (multiset.count b s) b

source

theorem multiset.filter_eq {α : Type u_1} [decidable_eq α] (s : multiset α) (b : α) :

multiset.filter (eq b) s = multiset.replicate (multiset.count b s) b

source

@[simp]

theorem multiset.replicate_inter {α : Type u_1} [decidable_eq α] (n : ℕ) (x : α) (s : multiset α) :

multiset.replicate n x ∩ s = multiset.replicate (linear_order.min n (multiset.count x s)) x

source

@[simp]

theorem multiset.inter_replicate {α : Type u_1} [decidable_eq α] (s : multiset α) (x : α) (n : ℕ) :

s ∩ multiset.replicate n x = multiset.replicate (linear_order.min (multiset.count x s) n) x

source

@[ext]

theorem multiset.add_hom_ext {α : Type u_1} {β : Type u_2} [add_zero_class β] ⦃f g : multiset α →+ β⦄ (h : ∀ (x : α), ⇑f {x} = ⇑g {x}) :

f = g

source

@[simp]

theorem multiset.map_le_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {s t : multiset α} :

multiset.map f s ≤ multiset.map f t ↔ s ≤ t

source

@[simp]

theorem multiset.map_embedding_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : multiset α) :

⇑(multiset.map_embedding f) s = multiset.map ⇑f s

source

def multiset.map_embedding {α : Type u_1} {β : Type u_2} (f : α ↪ β) :

multiset α ↪o multiset β

Associate to an embedding f from α to β the order embedding that maps a multiset to its image under f.

Equations

multiset.map_embedding f = order_embedding.of_map_le_iff (multiset.map ⇑f) _

source

theorem multiset.count_eq_card_filter_eq {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :

multiset.count a s = ⇑multiset.card (multiset.filter (eq a) s)

source

@[simp]

theorem multiset.map_count_true_eq_filter_card {α : Type u_1} (s : multiset α) (p : α → Prop) [decidable_pred p] :

multiset.count true (multiset.map p s) = ⇑multiset.card (multiset.filter p s)

Mapping a multiset through a predicate and counting the trues yields the cardinality of the set filtered by the predicate. Note that this uses the notion of a multiset of Props - due to the decidability requirements of count, the decidability instance on the LHS is different from the RHS. In particular, the decidability instance on the left leaks classical.dec_eq. See here for more discussion.

source

theorem multiset.rel_iff {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (ᾰ : multiset α) (ᾰ_1 : multiset β) :

multiset.rel r ᾰ ᾰ_1 ↔ ᾰ = 0 ∧ ᾰ_1 = 0 ∨ ∃ {a : α} {b : β} {as : multiset α} {bs : multiset β}, r a b ∧ multiset.rel r as bs ∧ ᾰ = a ::ₘ as ∧ ᾰ_1 = b ::ₘ bs

source

inductive multiset.rel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :

multiset α → multiset β → Prop

zero : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, multiset.rel r 0 0
cons : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β} {as : multiset α} {bs : multiset β}, r a b → multiset.rel r as bs → multiset.rel r (a ::ₘ as) (b ::ₘ bs)

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 betweem elements in s and t following r.

source

theorem multiset.rel_flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset β} {t : multiset α} :

multiset.rel (flip r) s t ↔ multiset.rel r t s

source

theorem multiset.rel_refl_of_refl_on {α : Type u_1} {m : multiset α} {r : α → α → Prop} :

(∀ (x : α), x ∈ m → r x x) → multiset.rel r m m

source

theorem multiset.rel_eq_refl {α : Type u_1} {s : multiset α} :

multiset.rel eq s s

source

theorem multiset.rel_eq {α : Type u_1} {s t : multiset α} :

multiset.rel eq s t ↔ s = t

source

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

multiset.rel p s t

source

theorem multiset.rel.add {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset α} {t : multiset β} {u : multiset α} {v : multiset β} (hst : multiset.rel r s t) (huv : multiset.rel r u v) :

multiset.rel r (s + u) (t + v)

source

theorem multiset.rel_flip_eq {α : Type u_1} {s t : multiset α} :

multiset.rel (λ (a b : α), b = a) s t ↔ s = t

source

@[simp]

theorem multiset.rel_zero_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {b : multiset β} :

multiset.rel r 0 b ↔ b = 0

source

@[simp]

theorem multiset.rel_zero_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : multiset α} :

multiset.rel r a 0 ↔ a = 0

source

theorem multiset.rel_cons_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {as : multiset α} {bs : multiset β} :

multiset.rel r (a ::ₘ as) bs ↔ ∃ (b : β) (bs' : multiset β), r a b ∧ multiset.rel r as bs' ∧ bs = b ::ₘ bs'

source

theorem multiset.rel_cons_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {as : multiset α} {b : β} {bs : multiset β} :

multiset.rel r as (b ::ₘ bs) ↔ ∃ (a : α) (as' : multiset α), r a b ∧ multiset.rel r as' bs ∧ as = a ::ₘ as'

source

theorem multiset.rel_add_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {as₀ as₁ : multiset α} {bs : multiset β} :

multiset.rel r (as₀ + as₁) bs ↔ ∃ (bs₀ bs₁ : multiset β), multiset.rel r as₀ bs₀ ∧ multiset.rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

source

theorem multiset.rel_add_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {as : multiset α} {bs₀ bs₁ : multiset β} :

multiset.rel r as (bs₀ + bs₁) ↔ ∃ (as₀ as₁ : multiset α), multiset.rel r as₀ bs₀ ∧ multiset.rel r as₁ bs₁ ∧ as = as₀ + as₁

source

theorem multiset.rel_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : multiset γ} {f : γ → α} {t : multiset β} :

multiset.rel r (multiset.map f s) t ↔ multiset.rel (λ (a : γ) (b : β), r (f a) b) s t

source

theorem multiset.rel_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : multiset α} {t : multiset γ} {f : γ → β} :

multiset.rel r s (multiset.map f t) ↔ multiset.rel (λ (a : α) (b : γ), r a (f b)) s t

source

theorem multiset.rel_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {p : γ → δ → Prop} {s : multiset α} {t : multiset β} {f : α → γ} {g : β → δ} :

multiset.rel p (multiset.map f s) (multiset.map g t) ↔ multiset.rel (λ (a : α) (b : β), p (f a) (g b)) s t

source

theorem multiset.card_eq_card_of_rel {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset α} {t : multiset β} (h : multiset.rel r s t) :

⇑multiset.card s = ⇑multiset.card t

source

theorem multiset.exists_mem_of_rel_of_mem {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset α} {t : multiset β} (h : multiset.rel r s t) {a : α} (ha : a ∈ s) :

∃ (b : β) (H : b ∈ t), r a b

source

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

multiset.rel r m1 m2

source

theorem multiset.rel_replicate_left {α : Type u_1} {m : multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :

multiset.rel r (multiset.replicate n a) m ↔ ⇑multiset.card m = n ∧ ∀ (x : α), x ∈ m → r a x

source

theorem multiset.rel_replicate_right {α : Type u_1} {m : multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :

multiset.rel r m (multiset.replicate n a) ↔ ⇑multiset.card m = n ∧ ∀ (x : α), x ∈ m → r x a

source

theorem multiset.rel.trans {α : Type u_1} (r : α → α → Prop) [is_trans α r] {s t u : multiset α} (r1 : multiset.rel r s t) (r2 : multiset.rel r t u) :

multiset.rel r s u

source

theorem multiset.rel.countp_eq {α : Type u_1} (r : α → α → Prop) [is_trans α r] [is_symm α r] {s t : multiset α} (x : α) [decidable_pred (r x)] (h : multiset.rel r s t) :

multiset.countp (r x) s = multiset.countp (r x) t

source

theorem multiset.map_eq_map {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {s t : multiset α} :

multiset.map f s = multiset.map f t ↔ s = t

source

theorem multiset.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) :

function.injective (multiset.map f)

source

theorem multiset.filter_attach' {α : Type u_1} (s : multiset α) (p : {a // a ∈ s} → Prop) [decidable_eq α] [decidable_pred p] :

multiset.filter p s.attach = multiset.map (subtype.map id _) (multiset.filter (λ (x : α), ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

source

theorem multiset.map_mk_eq_map_mk_of_rel {α : Type u_1} {r : α → α → Prop} {s t : multiset α} (hst : multiset.rel r s t) :

multiset.map (quot.mk r) s = multiset.map (quot.mk r) t

source

theorem multiset.exists_multiset_eq_map_quot_mk {α : Type u_1} {r : α → α → Prop} (s : multiset (quot r)) :

∃ (t : multiset α), s = multiset.map (quot.mk r) t

source

theorem multiset.induction_on_multiset_quot {α : Type u_1} {r : α → α → Prop} {p : multiset (quot r) → Prop} (s : multiset (quot r)) :

(∀ (s : multiset α), p (multiset.map (quot.mk r) s)) → p s

source

def multiset.disjoint {α : Type u_1} (s t : multiset α) :

Prop

disjoint s t means that s and t have no elements in common.

Equations

s.disjoint t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t → false

source

@[simp]

theorem multiset.coe_disjoint {α : Type u_1} (l₁ l₂ : list α) :

↑l₁.disjoint ↑l₂ ↔ l₁.disjoint l₂

source

theorem multiset.disjoint.symm {α : Type u_1} {s t : multiset α} (d : s.disjoint t) :

t.disjoint s

source

theorem multiset.disjoint_comm {α : Type u_1} {s t : multiset α} :

s.disjoint t ↔ t.disjoint s

source

theorem multiset.disjoint_left {α : Type u_1} {s t : multiset α} :

s.disjoint t ↔ ∀ {a : α}, a ∈ s → a ∉ t

source

theorem multiset.disjoint_right {α : Type u_1} {s t : multiset α} :

s.disjoint t ↔ ∀ {a : α}, a ∈ t → a ∉ s

source

theorem multiset.disjoint_iff_ne {α : Type u_1} {s t : multiset α} :

s.disjoint t ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b

source

theorem multiset.disjoint_of_subset_left {α : Type u_1} {s t u : multiset α} (h : s ⊆ u) (d : u.disjoint t) :

s.disjoint t

source

theorem multiset.disjoint_of_subset_right {α : Type u_1} {s t u : multiset α} (h : t ⊆ u) (d : s.disjoint u) :

s.disjoint t

source

theorem multiset.disjoint_of_le_left {α : Type u_1} {s t u : multiset α} (h : s ≤ u) :

u.disjoint t → s.disjoint t

source

theorem multiset.disjoint_of_le_right {α : Type u_1} {s t u : multiset α} (h : t ≤ u) :

s.disjoint u → s.disjoint t

source

@[simp]

theorem multiset.zero_disjoint {α : Type u_1} (l : multiset α) :

0.disjoint l

source

@[simp]

theorem multiset.singleton_disjoint {α : Type u_1} {l : multiset α} {a : α} :

{a}.disjoint l ↔ a ∉ l

source

@[simp]

theorem multiset.disjoint_singleton {α : Type u_1} {l : multiset α} {a : α} :

l.disjoint {a} ↔ a ∉ l

source

@[simp]

theorem multiset.disjoint_add_left {α : Type u_1} {s t u : multiset α} :

(s + t).disjoint u ↔ s.disjoint u ∧ t.disjoint u

source

@[simp]

theorem multiset.disjoint_add_right {α : Type u_1} {s t u : multiset α} :

s.disjoint (t + u) ↔ s.disjoint t ∧ s.disjoint u

source

@[simp]

theorem multiset.disjoint_cons_left {α : Type u_1} {a : α} {s t : multiset α} :

(a ::ₘ s).disjoint t ↔ a ∉ t ∧ s.disjoint t

source

@[simp]

theorem multiset.disjoint_cons_right {α : Type u_1} {a : α} {s t : multiset α} :

s.disjoint (a ::ₘ t) ↔ a ∉ s ∧ s.disjoint t

source

theorem multiset.inter_eq_zero_iff_disjoint {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s ∩ t = 0 ↔ s.disjoint t

source

@[simp]

theorem multiset.disjoint_union_left {α : Type u_1} [decidable_eq α] {s t u : multiset α} :

(s ∪ t).disjoint u ↔ s.disjoint u ∧ t.disjoint u

source

@[simp]

theorem multiset.disjoint_union_right {α : Type u_1} [decidable_eq α] {s t u : multiset α} :

s.disjoint (t ∪ u) ↔ s.disjoint t ∧ s.disjoint u

source

theorem multiset.add_eq_union_iff_disjoint {α : Type u_1} [decidable_eq α] {s t : multiset α} :

s + t = s ∪ t ↔ s.disjoint t

source

theorem multiset.disjoint_map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {s : multiset α} {t : multiset β} :

(multiset.map f s).disjoint (multiset.map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b

source

def multiset.pairwise {α : Type u_1} (r : α → α → Prop) (m : multiset α) :

Prop

pairwise r m states that there exists a list of the elements s.t. r holds pairwise on this list.

Equations

multiset.pairwise r m = ∃ (l : list α), m = ↑l ∧ list.pairwise r l

source

@[simp]

theorem multiset.pairwise_zero {α : Type u_1} (r : α → α → Prop) :

multiset.pairwise r 0

source

theorem multiset.pairwise_coe_iff {α : Type u_1} {r : α → α → Prop} {l : list α} :

multiset.pairwise r ↑l ↔ ∃ (l' : list α), l ~ l' ∧ list.pairwise r l'

source

theorem multiset.pairwise_coe_iff_pairwise {α : Type u_1} {r : α → α → Prop} (hr : symmetric r) {l : list α} :

multiset.pairwise r ↑l ↔ list.pairwise r l

source

theorem multiset.map_set_pairwise {α : Type u_1} {β : Type u_2} {f : α → β} {r : β → β → Prop} {m : multiset α} (h : {a : α | a ∈ m}.pairwise (λ (a₁ a₂ : α), r (f a₁) (f a₂))) :

{b : β | b ∈ multiset.map f m}.pairwise r

source