mathlib docs: data.multiset.finset

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

ndinsert a s is the lift of the list insert operation. This operation does not respect multiplicities, unlike cons, but it is suitable as an insert operation on finset.

Equations

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

source

@[simp]

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

multiset.ndinsert a ↑l = ↑(has_insert.insert a l)

source

@[simp]

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

multiset.ndinsert a 0 = a :: 0

source

@[simp]

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

a ∈ s → multiset.ndinsert a s = s

source

@[simp]

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

a ∉ s → multiset.ndinsert a s = a :: s

source

@[simp]

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

a ∈ multiset.ndinsert b s ↔ a = b ∨ a ∈ s

source

@[simp]

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

s ≤ multiset.ndinsert a s

source

@[simp]

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

a ∈ multiset.ndinsert a s

source

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

a ∈ s → a ∈ multiset.ndinsert b s

source

@[simp]

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

a ∈ s → (multiset.ndinsert a s).card = s.card

source

@[simp]

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

a ∉ s → (multiset.ndinsert a s).card = s.card + 1

source

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

(a :: s).erase_dup = multiset.ndinsert a s.erase_dup

source

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

s.nodup → (multiset.ndinsert a s).nodup

source

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

multiset.ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t

source

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

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

source

@[simp]

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

(multiset.ndinsert a s).disjoint t ↔ a ∉ t ∧ s.disjoint t

source

@[simp]

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

s.disjoint (multiset.ndinsert a t) ↔ a ∉ s ∧ s.disjoint t

source

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

multiset α → multiset α → multiset α

ndunion s t is the lift of the list union operation. This operation does not respect multiplicities, unlike s ∪ t, but it is suitable as a union operation on finset. (s ∪ t would also work as a union operation on finset, but this is more efficient.)

Equations

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

source

@[simp]

theorem multiset.coe_ndunion {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :

↑l₁.ndunion ↑l₂ = ↑(l₁ ∪ l₂)

source

@[simp]

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

0.ndunion s = s

source

@[simp]

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

(a :: s).ndunion t = multiset.ndinsert a (s.ndunion t)

source

@[simp]

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

a ∈ s.ndunion t ↔ a ∈ s ∨ a ∈ t

source

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

t ≤ s.ndunion t

source

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

t ⊆ s.ndunion t

source

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

s.ndunion t ≤ s + t

source

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

s.ndunion t ≤ u ↔ s ⊆ u ∧ t ≤ u

source

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

s ⊆ s.ndunion t

source

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

s.nodup → s ≤ s.ndunion t

source

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

s.ndunion t ≤ s ∪ t

source

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

t.nodup → (s.ndunion t).nodup

source

@[simp]

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

s.nodup → s.ndunion t = s ∪ t

source

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

(s + t).erase_dup = s.ndunion t.erase_dup

source

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

multiset α → multiset α → multiset α

ndinter s t is the lift of the list ∩ operation. This operation does not respect multiplicities, unlike s ∩ t, but it is suitable as an intersection operation on finset. (s ∩ t would also work as a union operation on finset, but this is more efficient.)

Equations

s.ndinter t = multiset.filter (λ (_x : α), _x ∈ t) s

source

@[simp]

theorem multiset.coe_ndinter {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :

↑l₁.ndinter ↑l₂ = ↑(l₁ ∩ l₂)

source

@[simp]

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

0.ndinter s = 0

source

@[simp]

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

a ∈ t → (a :: s).ndinter t = a :: s.ndinter t

source

@[simp]

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

a ∉ t → (a :: s).ndinter t = s.ndinter t

source

@[simp]

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

a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t

source

@[simp]

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

s.nodup → (s.ndinter t).nodup

source

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

s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u

source

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

s.ndinter t ≤ s

source

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

s.ndinter t ⊆ s

source

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

s.ndinter t ⊆ t

source

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

s.nodup → s.ndinter t ≤ t

source

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

s ∩ t ≤ s.ndinter t

source

@[simp]

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

s.nodup → s.ndinter t = s ∩ t

source

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

s.ndinter t = 0 ↔ s.disjoint t

mathlib documentation

data.multiset.finset_ops

Preparations for defining operations on `finset`.

finset insert

finset union

finset inter

General documentation

Additional documentation

Library

mathlib documentation

data.​multiset.​finset_ops

Preparations for defining operations on finset.

finset insert

finset union

finset inter

General documentation

Additional documentation

Library

data.multiset.finset_ops

Preparations for defining operations on `finset`.