mathlib3 documentation

data.multiset.finset_ops

Preparations for defining operations on finset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The operations here ignore multiplicities, and preparatory for defining the corresponding operations on finset.

finset insert #

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

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
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}
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 α} (h : a ∈ s) :
a ∈ multiset.ndinsert b s
source
@[simp]
theorem multiset.length_ndinsert_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (h : a ∈ s) :
⇑multiset.card (multiset.ndinsert a s) = ⇑multiset.card s
source
@[simp]
theorem multiset.length_ndinsert_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (h : a ∉ s) :
⇑multiset.card (multiset.ndinsert a s) = ⇑multiset.card s + 1
source
theorem multiset.dedup_cons {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
(a ::ₘ s).dedup = multiset.ndinsert a s.dedup
source
theorem multiset.nodup.ndinsert {α : Type u_1} [decidable_eq α] {s : multiset α} (a : α) :
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

finset union #

source
def multiset.ndunion {α : Type u_1} [decidable_eq α] (s t : 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
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 α) (d : 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 α} (d : s.nodup) :
s.ndunion t = s ∪ t
source
theorem multiset.dedup_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(s + t).dedup = s.ndunion t.dedup

finset inter #

source
def multiset.ndinter {α : Type u_1} [decidable_eq α] (s t : 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
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 α} (h : 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 α} (h : 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 α) (d : 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 α} (d : 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