Preparations for defining operations on Finset. #
The operations here ignore multiplicities,
and preparatory for defining the corresponding operations on Finset.
finset insert #
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.liftOn s (fun l => ↑(List.insert a l)) (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → Quot.mk Setoid.r (List.insert a x) = Quot.mk Setoid.r (List.insert a x_1))
@[simp]
theorem
Multiset.coe_ndinsert
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
Multiset.ndinsert a ↑l = ↑(insert a l)
@[simp]
theorem
Multiset.ndinsert_zero
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
:
Multiset.ndinsert a 0 = {a}
@[simp]
theorem
Multiset.ndinsert_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
:
a ∈ s → Multiset.ndinsert a s = s
@[simp]
theorem
Multiset.ndinsert_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
:
¬a ∈ s → Multiset.ndinsert a s = a ::ₘ s
@[simp]
theorem
Multiset.mem_ndinsert
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
{s : Multiset α}
:
@[simp]
theorem
Multiset.le_ndinsert_self
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(s : Multiset α)
:
s ≤ Multiset.ndinsert a s
theorem
Multiset.mem_ndinsert_self
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(s : Multiset α)
:
a ∈ Multiset.ndinsert a s
theorem
Multiset.mem_ndinsert_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
{s : Multiset α}
(h : a ∈ s)
:
a ∈ Multiset.ndinsert b s
@[simp]
theorem
Multiset.length_ndinsert_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
(h : a ∈ s)
:
↑Multiset.card (Multiset.ndinsert a s) = ↑Multiset.card s
@[simp]
theorem
Multiset.length_ndinsert_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
(h : ¬a ∈ s)
:
↑Multiset.card (Multiset.ndinsert a s) = ↑Multiset.card s + 1
theorem
Multiset.dedup_cons
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
:
Multiset.dedup (a ::ₘ s) = Multiset.ndinsert a (Multiset.dedup s)
theorem
Multiset.Nodup.ndinsert
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
(a : α)
:
Multiset.Nodup s → Multiset.Nodup (Multiset.ndinsert a s)
theorem
Multiset.ndinsert_le
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
{t : Multiset α}
:
theorem
Multiset.attach_ndinsert
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(s : Multiset α)
:
Multiset.attach (Multiset.ndinsert a s) = Multiset.ndinsert { val := a, property := (_ : a ∈ Multiset.ndinsert a s) }
(Multiset.map (fun p => { val := ↑p, property := (_ : ↑p ∈ Multiset.ndinsert a s) }) (Multiset.attach s))
@[simp]
theorem
Multiset.disjoint_ndinsert_left
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
{t : Multiset α}
:
Multiset.Disjoint (Multiset.ndinsert a s) t ↔ ¬a ∈ t ∧ Multiset.Disjoint s t
@[simp]
theorem
Multiset.disjoint_ndinsert_right
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{s : Multiset α}
{t : Multiset α}
:
Multiset.Disjoint s (Multiset.ndinsert a t) ↔ ¬a ∈ s ∧ Multiset.Disjoint s t
finset union #
def
Multiset.ndunion
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset α
ndunion s t is the lift of the list union operation. This operation
does not respect multiplicities, unlike s ∪ t∪ t, but it is suitable as
a union operation on Finset. (s ∪ t∪ t would also work as a union operation
on finset, but this is more efficient.)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Multiset.coe_ndunion
{α : Type u_1}
[inst : DecidableEq α]
(l₁ : List α)
(l₂ : List α)
:
Multiset.ndunion ↑l₁ ↑l₂ = ↑(l₁ ∪ l₂)
theorem
Multiset.zero_ndunion
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
:
Multiset.ndunion 0 s = s
@[simp]
theorem
Multiset.cons_ndunion
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
(a : α)
:
Multiset.ndunion (a ::ₘ s) t = Multiset.ndinsert a (Multiset.ndunion s t)
@[simp]
theorem
Multiset.mem_ndunion
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
{a : α}
:
theorem
Multiset.le_ndunion_right
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
t ≤ Multiset.ndunion s t
theorem
Multiset.subset_ndunion_right
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
t ⊆ Multiset.ndunion s t
theorem
Multiset.ndunion_le_add
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset.ndunion s t ≤ s + t
theorem
Multiset.ndunion_le
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
{u : Multiset α}
:
theorem
Multiset.subset_ndunion_left
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
s ⊆ Multiset.ndunion s t
theorem
Multiset.le_ndunion_left
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
(t : Multiset α)
(d : Multiset.Nodup s)
:
s ≤ Multiset.ndunion s t
theorem
Multiset.ndunion_le_union
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset.ndunion s t ≤ s ∪ t
theorem
Multiset.Nodup.ndunion
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
{t : Multiset α}
:
Multiset.Nodup t → Multiset.Nodup (Multiset.ndunion s t)
@[simp]
theorem
Multiset.ndunion_eq_union
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
(d : Multiset.Nodup s)
:
Multiset.ndunion s t = s ∪ t
theorem
Multiset.dedup_add
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset.dedup (s + t) = Multiset.ndunion s (Multiset.dedup t)
finset inter #
def
Multiset.ndinter
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset α
ndinter s t is the lift of the list ∩∩ operation. This operation
does not respect multiplicities, unlike s ∩ t∩ t, but it is suitable as
an intersection operation on Finset. (s ∩ t∩ t would also work as a union operation
on finset, but this is more efficient.)
Equations
- Multiset.ndinter s t = Multiset.filter (fun x => x ∈ t) s
@[simp]
theorem
Multiset.coe_ndinter
{α : Type u_1}
[inst : DecidableEq α]
(l₁ : List α)
(l₂ : List α)
:
Multiset.ndinter ↑l₁ ↑l₂ = ↑(l₁ ∩ l₂)
@[simp]
theorem
Multiset.zero_ndinter
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
:
Multiset.ndinter 0 s = 0
@[simp]
theorem
Multiset.cons_ndinter_of_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
(s : Multiset α)
{t : Multiset α}
(h : a ∈ t)
:
Multiset.ndinter (a ::ₘ s) t = a ::ₘ Multiset.ndinter s t
@[simp]
theorem
Multiset.ndinter_cons_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
(s : Multiset α)
{t : Multiset α}
(h : ¬a ∈ t)
:
Multiset.ndinter (a ::ₘ s) t = Multiset.ndinter s t
@[simp]
theorem
Multiset.mem_ndinter
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
{a : α}
:
@[simp]
theorem
Multiset.Nodup.ndinter
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
(t : Multiset α)
:
Multiset.Nodup s → Multiset.Nodup (Multiset.ndinter s t)
theorem
Multiset.le_ndinter
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
{u : Multiset α}
:
theorem
Multiset.ndinter_le_left
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset.ndinter s t ≤ s
theorem
Multiset.ndinter_subset_left
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset.ndinter s t ⊆ s
theorem
Multiset.ndinter_subset_right
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
Multiset.ndinter s t ⊆ t
theorem
Multiset.ndinter_le_right
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
(t : Multiset α)
(d : Multiset.Nodup s)
:
Multiset.ndinter s t ≤ t
theorem
Multiset.inter_le_ndinter
{α : Type u_1}
[inst : DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
s ∩ t ≤ Multiset.ndinter s t
@[simp]
theorem
Multiset.ndinter_eq_inter
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
(d : Multiset.Nodup s)
:
Multiset.ndinter s t = s ∩ t
theorem
Multiset.ndinter_eq_zero_iff_disjoint
{α : Type u_1}
[inst : DecidableEq α]
{s : Multiset α}
{t : Multiset α}
:
Multiset.ndinter s t = 0 ↔ Multiset.Disjoint s t