Module docstring
{"# Preparations for defining operations on Finset.
The operations here ignore multiplicities,
and preparatory for defining the corresponding operations on Finset.
","### finset insert ","### finset union ","### finset inter "}
Multiset.ndinsert
definition
(a : α) (s : Multiset α) : Multiset α
Full source
/-- `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`. -/
def ndinsert (a : α) (s : Multiset α) : Multiset α :=
Quot.liftOn s (fun l => (l.insert a : Multiset α)) fun _ _ p => Quot.sound (p.insert a)Informal description
The function `ndinsert a s` inserts an element `a` into the multiset `s`, ignoring multiplicities. It is the multiset version of the list `insert` operation, suitable for use with `Finset`.
Multiset.coe_ndinsert
theorem
(a : α) (l : List α) : ndinsert a l = (insert a l : List α)
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the multiset obtained by inserting $a$ into $l$ (ignoring multiplicities) is equal to the multiset corresponding to the list obtained by inserting $a$ into $l$, i.e., $\text{ndinsert}(a, l) = \text{ofList}(\text{insert}(a, l))$.
Multiset.ndinsert_zero
theorem
(a : α) : ndinsert a 0 = { a }
Full source
@[simp]
theorem ndinsert_zero (a : α) : ndinsert a 0 = {a} :=
rflInformal description
For any element $a$ of type $\alpha$, inserting $a$ into the empty multiset results in a singleton multiset containing $a$, i.e., $\text{ndinsert}(a, 0) = \{a\}$.
Multiset.ndinsert_of_mem
theorem
{a : α} {s : Multiset α} : a ∈ s → ndinsert a s = s
Full source
@[simp]
theorem ndinsert_of_mem {a : α} {s : Multiset α} : a ∈ s → ndinsert a s = s :=
Quot.inductionOn s fun _ h => congr_arg ((↑) : List α → Multiset α) <| insert_of_mem hInformal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is a member of $s$, then inserting $a$ into $s$ (ignoring multiplicities) leaves $s$ unchanged, i.e., $\text{ndinsert}(a, s) = s$.
Multiset.ndinsert_of_not_mem
theorem
{a : α} {s : Multiset α} : a ∉ s → ndinsert a s = a ::ₘ s
Full source
@[simp]
theorem ndinsert_of_not_mem {a : α} {s : Multiset α} : a ∉ s → ndinsert a s = a ::ₘ s :=
Quot.inductionOn s fun _ h => congr_arg ((↑) : List α → Multiset α) <| insert_of_not_mem hInformal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is not a member of $s$, then inserting $a$ into $s$ (ignoring multiplicities) results in the multiset obtained by adding one occurrence of $a$ to $s$, i.e., $\text{ndinsert}(a, s) = a \cup s$.
Multiset.mem_ndinsert
theorem
{a b : α} {s : Multiset α} : a ∈ ndinsert b s ↔ a = b ∨ a ∈ s
Full source
@[simp]
theorem mem_ndinsert {a b : α} {s : Multiset α} : a ∈ ndinsert b sa ∈ ndinsert b s ↔ a = b ∨ a ∈ s :=
Quot.inductionOn s fun _ => mem_insert_iffInformal description
For any elements $a, b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the element $a$ is in the multiset obtained by inserting $b$ into $s$ (ignoring multiplicities) if and only if $a$ equals $b$ or $a$ is already in $s$. In symbols:
$$a \in \text{ndinsert}(b, s) \leftrightarrow (a = b \lor a \in s).$$
Multiset.le_ndinsert_self
theorem
(a : α) (s : Multiset α) : s ≤ ndinsert a s
Full source
@[simp]
theorem le_ndinsert_self (a : α) (s : Multiset α) : s ≤ ndinsert a s :=
Quot.inductionOn s fun _ => (sublist_insert _ _).subpermInformal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multiset $s$ is a sub-multiset of the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities). In symbols:
$$s \leq \text{ndinsert}(a, s).$$
Multiset.mem_ndinsert_self
theorem
(a : α) (s : Multiset α) : a ∈ ndinsert a s
Full source
theorem mem_ndinsert_self (a : α) (s : Multiset α) : a ∈ ndinsert a s := by simpInformal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the element $a$ is contained in the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities). In symbols:
$$a \in \text{ndinsert}(a, s).$$
Multiset.mem_ndinsert_of_mem
theorem
{a b : α} {s : Multiset α} (h : a ∈ s) : a ∈ ndinsert b s
Full source
theorem mem_ndinsert_of_mem {a b : α} {s : Multiset α} (h : a ∈ s) : a ∈ ndinsert b s :=
mem_ndinsert.2 (Or.inr h)Informal description
For any elements $a, b$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is a member of $s$, then $a$ is also a member of the multiset obtained by inserting $b$ into $s$ (ignoring multiplicities). In symbols:
$$a \in s \implies a \in \text{ndinsert}(b, s).$$
Multiset.length_ndinsert_of_mem
theorem
{a : α} {s : Multiset α} (h : a ∈ s) : card (ndinsert a s) = card s
Informal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is a member of $s$, then the cardinality of the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities) is equal to the cardinality of $s$, i.e., $|\text{ndinsert}(a, s)| = |s|$.
Multiset.length_ndinsert_of_not_mem
theorem
{a : α} {s : Multiset α} (h : a ∉ s) : card (ndinsert a s) = card s + 1
Informal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is not a member of $s$, then the cardinality of the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities) is equal to the cardinality of $s$ plus one, i.e., $|\text{ndinsert}(a, s)| = |s| + 1$.
Multiset.dedup_cons
theorem
{a : α} {s : Multiset α} : dedup (a ::ₘ s) = ndinsert a (dedup s)
Full source
theorem dedup_cons {a : α} {s : Multiset α} : dedup (a ::ₘ s) = ndinsert a (dedup s) := by
by_cases h : a ∈ s <;> simp [h]Informal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the deduplication of the multiset obtained by inserting $a$ into $s$ is equal to inserting $a$ into the deduplication of $s$ (ignoring multiplicities). In symbols:
\[ \text{dedup}(a \cons s) = \text{ndinsert}(a, \text{dedup}(s)). \]
Multiset.Nodup.ndinsert
theorem
(a : α) : Nodup s → Nodup (ndinsert a s)
Full source
theorem Nodup.ndinsert (a : α) : Nodup s → Nodup (ndinsert a s) :=
Quot.inductionOn s fun _ => Nodup.insertInformal description
For any multiset $s$ over a type $\alpha$ with no duplicate elements (i.e., $\text{Nodup}(s)$), and for any element $a \in \alpha$, the multiset obtained by inserting $a$ into $s$ (denoted as $\text{ndinsert}(a, s)$) also has no duplicate elements.
Multiset.ndinsert_le
theorem
{a : α} {s t : Multiset α} : ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t
Full source
theorem ndinsert_le {a : α} {s t : Multiset α} : ndinsertndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t :=
⟨fun h => ⟨le_trans (le_ndinsert_self _ _) h, mem_of_le h (mem_ndinsert_self _ _)⟩, fun ⟨l, m⟩ =>
if h : a ∈ s then by simp [h, l]
else by
rw [ndinsert_of_not_mem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_not_mem h,
cons_erase m]
exact l⟩Informal description
For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities) is a submultiset of $t$ if and only if $s$ is a submultiset of $t$ and $a$ is an element of $t$. In symbols:
$$ \text{ndinsert}(a, s) \leq t \leftrightarrow s \leq t \land a \in t. $$
Multiset.attach_ndinsert
theorem
(a : α) (s : Multiset α) :
(s.ndinsert a).attach = ndinsert ⟨a, mem_ndinsert_self a s⟩ (s.attach.map fun p => ⟨p.1, mem_ndinsert_of_mem p.2⟩)
Full source
theorem attach_ndinsert (a : α) (s : Multiset α) :
(s.ndinsert a).attach =
ndinsert ⟨a, mem_ndinsert_self a s⟩ (s.attach.map fun p => ⟨p.1, mem_ndinsert_of_mem p.2⟩) :=
have eq :
∀ h : ∀ p : { x // x ∈ s }, p.1 ∈ s,
(fun p : { x // x ∈ s } => ⟨p.val, h p⟩ : { x // x ∈ s } → { x // x ∈ s }) = id :=
fun _ => funext fun _ => Subtype.eq rfl
have : ∀ (t) (eq : s.ndinsert a = t), t.attach = ndinsert ⟨a, eq ▸ mem_ndinsert_self a s⟩
(s.attach.map fun p => ⟨p.1, eq ▸ mem_ndinsert_of_mem p.2⟩) := by
intro t ht
by_cases h : a ∈ s
· rw [ndinsert_of_mem h] at ht
subst ht
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
· rw [ndinsert_of_not_mem h] at ht
subst ht
simp [attach_cons, h]
this _ rflInformal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the attached multiset of $\text{ndinsert}(a, s)$ is equal to the multiset obtained by:
1. Inserting the pair $\langle a, h \rangle$ where $h$ is the proof that $a \in \text{ndinsert}(a, s)$, and
2. Mapping each element $\langle x, h_x \rangle$ in the attached multiset of $s$ to $\langle x, h'_x \rangle$ where $h'_x$ is the proof that $x \in \text{ndinsert}(a, s)$ derived from $h_x$ (the original proof that $x \in s$).
Multiset.disjoint_ndinsert_left
theorem
{a : α} {s t : Multiset α} : Disjoint (ndinsert a s) t ↔ a ∉ t ∧ Disjoint s t
Full source
@[simp]
theorem disjoint_ndinsert_left {a : α} {s t : Multiset α} :
DisjointDisjoint (ndinsert a s) t ↔ a ∉ t ∧ Disjoint s t :=
Iff.trans (by simp [disjoint_left]) disjoint_cons_leftInformal description
For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities) is disjoint from $t$ if and only if $a$ does not belong to $t$ and $s$ is disjoint from $t$. In symbols:
$$ \text{ndinsert}(a, s) \mathbin{\#} t \leftrightarrow a \notin t \land s \mathbin{\#} t $$
where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_ndinsert_right
theorem
{a : α} {s t : Multiset α} : Disjoint s (ndinsert a t) ↔ a ∉ s ∧ Disjoint s t
Full source
@[simp]
theorem disjoint_ndinsert_right {a : α} {s t : Multiset α} :
DisjointDisjoint s (ndinsert a t) ↔ a ∉ s ∧ Disjoint s t := by
rw [_root_.disjoint_comm, disjoint_ndinsert_left]; tautoInformal description
For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the multiset $s$ is disjoint from the multiset obtained by inserting $a$ into $t$ (ignoring multiplicities) if and only if $a$ does not belong to $s$ and $s$ is disjoint from $t$. In symbols:
$$ s \mathbin{\#} \text{ndinsert}(a, t) \leftrightarrow a \notin s \land s \mathbin{\#} t $$
where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.ndunion
definition
(s t : Multiset α) : Multiset α
Full source
/-- `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.) -/
def ndunion (s t : Multiset α) : Multiset α :=
(Quotient.liftOn₂ s t fun l₁ l₂ => (l₁.union l₂ : Multiset α)) fun _ _ _ _ p₁ p₂ =>
Quot.sound <| p₁.union p₂Informal description
The function `ndunion s t` constructs the union of two multisets `s` and `t`, ignoring multiplicities of elements. It is defined as the lift of the list union operation to multisets via quotienting by permutation equivalence. Specifically, for lists `l₁` and `l₂`, the union `ndunion ⟦l₁⟧ ⟦l₂⟧` is equal to the multiset `⟦l₁ ∪ l₂⟧`, where `⟦·⟧` denotes the equivalence class under permutation.
Multiset.coe_ndunion
theorem
(l₁ l₂ : List α) : @ndunion α _ l₁ l₂ = (l₁ ∪ l₂ : List α)
Informal description
For any two lists `l₁` and `l₂` of elements of type `α`, the multiset union (ignoring multiplicities) of their corresponding multisets is equal to the multiset corresponding to the list union of `l₁` and `l₂`. In other words, the following equality holds:
$$ \text{ndunion}(\text{ofList}(l₁), \text{ofList}(l₂)) = \text{ofList}(l₁ ∪ l₂) $$
Multiset.zero_ndunion
theorem
(s : Multiset α) : ndunion 0 s = s
Full source
theorem zero_ndunion (s : Multiset α) : ndunion 0 s = s :=
Quot.inductionOn s fun _ => rflInformal description
For any multiset $s$ over a type $\alpha$, the union of the empty multiset $0$ with $s$ is equal to $s$, i.e., $\text{ndunion}(0, s) = s$.
Multiset.cons_ndunion
theorem
(s t : Multiset α) (a : α) : ndunion (a ::ₘ s) t = ndinsert a (ndunion s t)
Full source
@[simp]
theorem cons_ndunion (s t : Multiset α) (a : α) : ndunion (a ::ₘ s) t = ndinsert a (ndunion s t) :=
Quot.induction_on₂ s t fun _ _ => rflInformal description
For any multisets $s$ and $t$ over a type $\alpha$ and any element $a \in \alpha$, the union of the multiset obtained by inserting $a$ into $s$ (denoted $a ::ₘ s$) with $t$ is equal to inserting $a$ into the union of $s$ and $t$. That is:
$$ \text{ndunion}(a ::ₘ s, t) = \text{ndinsert}(a, \text{ndunion}(s, t)) $$
Multiset.mem_ndunion
theorem
{s t : Multiset α} {a : α} : a ∈ ndunion s t ↔ a ∈ s ∨ a ∈ t
Full source
@[simp]
theorem mem_ndunion {s t : Multiset α} {a : α} : a ∈ ndunion s ta ∈ ndunion s t ↔ a ∈ s ∨ a ∈ t :=
Quot.induction_on₂ s t fun _ _ => List.mem_union_iffInformal description
For any multisets $s$ and $t$ over a type $\alpha$ and any element $a \in \alpha$, the element $a$ belongs to the union of $s$ and $t$ (ignoring multiplicities) if and only if $a$ belongs to $s$ or $a$ belongs to $t$. In symbols:
$$ a \in \text{ndunion}(s, t) \leftrightarrow a \in s \lor a \in t $$
Multiset.le_ndunion_right
theorem
(s t : Multiset α) : t ≤ ndunion s t
Full source
theorem le_ndunion_right (s t : Multiset α) : t ≤ ndunion s t :=
Quot.induction_on₂ s t fun _ _ => (suffix_union_right _ _).sublist.subpermInformal description
For any two multisets $s$ and $t$ over a type $\alpha$, the multiset $t$ is a sub-multiset of the union of $s$ and $t$ (ignoring multiplicities). In symbols:
$$ t \leq \text{ndunion}(s, t) $$
Multiset.subset_ndunion_right
theorem
(s t : Multiset α) : t ⊆ ndunion s t
Full source
theorem subset_ndunion_right (s t : Multiset α) : t ⊆ ndunion s t :=
subset_of_le (le_ndunion_right s t)Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the multiset $t$ is a subset of the union of $s$ and $t$ (ignoring multiplicities). In symbols:
$$ t \subseteq \text{ndunion}(s, t) $$
Multiset.ndunion_le_add
theorem
(s t : Multiset α) : ndunion s t ≤ s + t
Full source
theorem ndunion_le_add (s t : Multiset α) : ndunion s t ≤ s + t :=
Quot.induction_on₂ s t fun _ _ => (union_sublist_append _ _).subpermInformal description
For any two multisets $s$ and $t$ over a type $\alpha$, the union of $s$ and $t$ (ignoring multiplicities) is a sub-multiset of their sum (which counts multiplicities). In symbols:
$$ \text{ndunion}(s, t) \leq s + t $$
Multiset.ndunion_le
theorem
{s t u : Multiset α} : ndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u
Full source
theorem ndunion_le {s t u : Multiset α} : ndunionndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u :=
Multiset.induction_on s (by simp [zero_ndunion])
(fun _ _ h =>
by simp only [cons_ndunion, mem_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h,
and_assoc])Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the union of $s$ and $t$ (ignoring multiplicities) is a sub-multiset of $u$ if and only if $s$ is a subset of $u$ and $t$ is a sub-multiset of $u$. In symbols:
$$ \text{ndunion}(s, t) \leq u \leftrightarrow s \subseteq u \land t \leq u $$
Multiset.subset_ndunion_left
theorem
(s t : Multiset α) : s ⊆ ndunion s t
Full source
theorem subset_ndunion_left (s t : Multiset α) : s ⊆ ndunion s t := fun _ h =>
mem_ndunion.2 <| Or.inl hInformal description
For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is a subset of the union of $s$ and $t$ (ignoring multiplicities). In symbols:
$$ s \subseteq \text{ndunion}(s, t) $$
Multiset.le_ndunion_left
theorem
{s} (t : Multiset α) (d : Nodup s) : s ≤ ndunion s t
Full source
theorem le_ndunion_left {s} (t : Multiset α) (d : Nodup s) : s ≤ ndunion s t :=
(le_iff_subset d).2 <| subset_ndunion_left _ _Informal description
For any duplicate-free multiset $s$ and any multiset $t$ over a type $\alpha$, the multiset $s$ is a sub-multiset of the union of $s$ and $t$ (ignoring multiplicities). In symbols:
$$ s \leq \text{ndunion}(s, t) $$
Multiset.ndunion_le_union
theorem
(s t : Multiset α) : ndunion s t ≤ s ∪ t
Full source
theorem ndunion_le_union (s t : Multiset α) : ndunion s t ≤ s ∪ t :=
ndunion_le.2 ⟨subset_of_le le_union_left, le_union_right⟩Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the union of $s$ and $t$ (ignoring multiplicities) is a sub-multiset of the union of $s$ and $t$ (with multiplicities). In symbols:
$$ \text{ndunion}(s, t) \leq s \cup t $$
Multiset.Nodup.ndunion
theorem
(s : Multiset α) {t : Multiset α} : Nodup t → Nodup (ndunion s t)
Full source
theorem Nodup.ndunion (s : Multiset α) {t : Multiset α} : Nodup t → Nodup (ndunion s t) :=
Quot.induction_on₂ s t fun _ _ => List.Nodup.union _Informal description
For any multiset $s$ and any multiset $t$ of elements of type $\alpha$, if $t$ has no duplicate elements, then the union of $s$ and $t$ (ignoring multiplicities) also has no duplicate elements.
Multiset.ndunion_eq_union
theorem
{s t : Multiset α} (d : Nodup s) : ndunion s t = s ∪ t
Full source
@[simp]
theorem ndunion_eq_union {s t : Multiset α} (d : Nodup s) : ndunion s t = s ∪ t :=
le_antisymm (ndunion_le_union _ _) <| union_le (le_ndunion_left _ d) (le_ndunion_right _ _)Informal description
For any multisets $s$ and $t$ over a type $\alpha$, if $s$ has no duplicate elements, then the union of $s$ and $t$ (ignoring multiplicities) is equal to the union of $s$ and $t$ (with multiplicities). In symbols:
$$ \text{ndunion}(s, t) = s \cup t $$
Multiset.dedup_add
theorem
(s t : Multiset α) : dedup (s + t) = ndunion s (dedup t)
Full source
theorem dedup_add (s t : Multiset α) : dedup (s + t) = ndunion s (dedup t) :=
Quot.induction_on₂ s t fun _ _ => congr_arg ((↑) : List α → Multiset α) <| dedup_append _ _Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the deduplication of their sum $s + t$ is equal to the union of $s$ with the deduplicated version of $t$, i.e., $\mathrm{dedup}(s + t) = \mathrm{ndunion}\, s\, (\mathrm{dedup}\, t)$.
Multiset.Disjoint.ndunion_eq
theorem
{s t : Multiset α} (h : Disjoint s t) : s.ndunion t = s.dedup + t
Full source
theorem Disjoint.ndunion_eq {s t : Multiset α} (h : Disjoint s t) :
s.ndunion t = s.dedup + t := by
induction s, t using Quot.induction_on₂
exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq <| by simpa using hInformal description
For any two multisets $s$ and $t$ over a type $\alpha$, if $s$ and $t$ are disjoint (i.e., they share no common elements), then the union of $s$ and $t$ (ignoring multiplicities) is equal to the sum of the deduplicated version of $s$ and $t$, i.e., $\mathrm{ndunion}\, s\, t = \mathrm{dedup}\, s + t$.
Multiset.Subset.ndunion_eq_right
theorem
{s t : Multiset α} (h : s ⊆ t) : s.ndunion t = t
Full source
theorem Subset.ndunion_eq_right {s t : Multiset α} (h : s ⊆ t) : s.ndunion t = t := by
induction s, t using Quot.induction_on₂
exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.union_eq_right hInformal description
For any two multisets $s$ and $t$ over a type $\alpha$, if $s$ is a subset of $t$ (i.e., every element of $s$ appears in $t$ with at least the same multiplicity), then the union of $s$ and $t$ (ignoring multiplicities) equals $t$, i.e., $s \mathbin{\mathrm{ndunion}} t = t$.
Multiset.ndinter
definition
(s t : Multiset α) : Multiset α
Full source
/-- `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.) -/
def ndinter (s t : Multiset α) : Multiset α :=
filter (· ∈ t) sInformal description
The function `ndinter s t` computes the intersection of two multisets `s` and `t` by filtering elements of `s` that are also in `t`. Unlike the standard multiset intersection, this operation does not preserve multiplicities, making it suitable for efficient operations on `Finset`.
Multiset.coe_ndinter
theorem
(l₁ l₂ : List α) : @ndinter α _ l₁ l₂ = (l₁ ∩ l₂ : List α)
Full source
@[simp]
theorem coe_ndinter (l₁ l₂ : List α) : @ndinter α _ l₁ l₂ = (l₁ ∩ l₂ : List α) := by
simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]
apply Perm.reflInformal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the non-multiplicity-preserving intersection of their corresponding multisets is equal to the list intersection of $l_1$ and $l_2$.
Multiset.zero_ndinter
theorem
(s : Multiset α) : ndinter 0 s = 0
Full source
@[simp]
theorem zero_ndinter (s : Multiset α) : ndinter 0 s = 0 :=
rflInformal description
For any multiset $s$ over a type $\alpha$, the intersection of the empty multiset $0$ with $s$ is the empty multiset, i.e., $\text{ndinter}(0, s) = 0$.
Multiset.cons_ndinter_of_mem
theorem
{a : α} (s : Multiset α) {t : Multiset α} (h : a ∈ t) : ndinter (a ::ₘ s) t = a ::ₘ ndinter s t
Full source
@[simp]
theorem cons_ndinter_of_mem {a : α} (s : Multiset α) {t : Multiset α} (h : a ∈ t) :
ndinter (a ::ₘ s) t = a ::ₘ ndinter s t := by simp [ndinter, h]Informal description
For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, if $a$ is a member of $t$, then the non-multiplicity-preserving intersection of the multiset obtained by inserting $a$ into $s$ (denoted $a ::ₘ s$) with $t$ is equal to the multiset obtained by inserting $a$ into the non-multiplicity-preserving intersection of $s$ and $t$. That is, $\text{ndinter}(a ::ₘ s, t) = a ::ₘ \text{ndinter}(s, t)$.
Multiset.ndinter_cons_of_not_mem
theorem
{a : α} (s : Multiset α) {t : Multiset α} (h : a ∉ t) : ndinter (a ::ₘ s) t = ndinter s t
Informal description
For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, if $a$ is not in $t$, then the non-multiplicity-preserving intersection of the multiset obtained by prepending $a$ to $s$ with $t$ is equal to the non-multiplicity-preserving intersection of $s$ with $t$. In symbols:
\[ \text{ndinter}(a \text{ ::ₘ } s, t) = \text{ndinter}(s, t) \quad \text{when} \quad a \notin t. \]
Multiset.mem_ndinter
theorem
{s t : Multiset α} {a : α} : a ∈ ndinter s t ↔ a ∈ s ∧ a ∈ t
Full source
@[simp]
theorem mem_ndinter {s t : Multiset α} {a : α} : a ∈ ndinter s ta ∈ ndinter s t ↔ a ∈ s ∧ a ∈ t := by
simp [ndinter, mem_filter]Informal description
For any multisets $s$ and $t$ over a type $\alpha$, and any element $a \in \alpha$, we have $a \in \text{ndinter}(s, t)$ if and only if $a$ belongs to both $s$ and $t$.
Multiset.Nodup.ndinter
theorem
{s : Multiset α} (t : Multiset α) : Nodup s → Nodup (ndinter s t)
Full source
@[simp]
theorem Nodup.ndinter {s : Multiset α} (t : Multiset α) : Nodup s → Nodup (ndinter s t) :=
Nodup.filter _Informal description
For any multiset $s$ over a type $\alpha$, if $s$ has no duplicate elements, then the intersection $\text{ndinter } s \ t$ of $s$ with any other multiset $t$ also has no duplicate elements.
Multiset.le_ndinter
theorem
{s t u : Multiset α} : s ≤ ndinter t u ↔ s ≤ t ∧ s ⊆ u
Full source
theorem le_ndinter {s t u : Multiset α} : s ≤ ndinter t u ↔ s ≤ t ∧ s ⊆ u := by
simp [ndinter, le_filter, subset_iff]Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the sub-multiset relation $s \leq \text{ndinter}(t, u)$ holds if and only if $s \leq t$ and $s \subseteq u$.
Multiset.ndinter_le_left
theorem
(s t : Multiset α) : ndinter s t ≤ s
Full source
theorem ndinter_le_left (s t : Multiset α) : ndinter s t ≤ s :=
(le_ndinter.1 le_rfl).1Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the non-multiplicity-preserving intersection $\text{ndinter}(s, t)$ is a sub-multiset of $s$, i.e., $\text{ndinter}(s, t) \leq s$.
Multiset.ndinter_subset_left
theorem
(s t : Multiset α) : ndinter s t ⊆ s
Full source
theorem ndinter_subset_left (s t : Multiset α) : ndinterndinter s t ⊆ s :=
subset_of_le (ndinter_le_left s t)Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the non-multiplicity-preserving intersection $\text{ndinter}(s, t)$ is a subset of $s$, i.e., every element in $\text{ndinter}(s, t)$ appears in $s$ (with nonzero multiplicity).
Multiset.ndinter_subset_right
theorem
(s t : Multiset α) : ndinter s t ⊆ t
Full source
theorem ndinter_subset_right (s t : Multiset α) : ndinterndinter s t ⊆ t :=
(le_ndinter.1 le_rfl).2Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the non-multiplicity-preserving intersection $\text{ndinter}(s, t)$ is a subset of $t$, i.e., every element in $\text{ndinter}(s, t)$ appears in $t$ (with nonzero multiplicity).
Multiset.ndinter_le_right
theorem
{s} (t : Multiset α) (d : Nodup s) : ndinter s t ≤ t
Full source
theorem ndinter_le_right {s} (t : Multiset α) (d : Nodup s) : ndinter s t ≤ t :=
(le_iff_subset <| d.ndinter _).2 <| ndinter_subset_right _ _Informal description
For any multiset $s$ over a type $\alpha$ with no duplicate elements, and any multiset $t$ over $\alpha$, the non-multiplicity-preserving intersection $\text{ndinter}(s, t)$ is a submultiset of $t$, i.e., $\text{ndinter}(s, t) \leq t$.
Multiset.inter_le_ndinter
theorem
(s t : Multiset α) : s ∩ t ≤ ndinter s t
Full source
theorem inter_le_ndinter (s t : Multiset α) : s ∩ t ≤ ndinter s t :=
le_ndinter.2 ⟨inter_le_left, subset_of_le inter_le_right⟩Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the standard intersection $s \cap t$ is a submultiset of the non-multiplicity-preserving intersection $\text{ndinter}(s, t)$.
Multiset.ndinter_eq_inter
theorem
{s t : Multiset α} (d : Nodup s) : ndinter s t = s ∩ t
Full source
@[simp]
theorem ndinter_eq_inter {s t : Multiset α} (d : Nodup s) : ndinter s t = s ∩ t :=
le_antisymm (le_inter (ndinter_le_left _ _) (ndinter_le_right _ d)) (inter_le_ndinter _ _)Informal description
For any multisets $s$ and $t$ over a type $\alpha$, if $s$ has no duplicate elements, then the non-multiplicity-preserving intersection $\text{ndinter}(s, t)$ is equal to the standard multiset intersection $s \cap t$.
Multiset.ndinter_eq_zero_iff_disjoint
theorem
{s t : Multiset α} : ndinter s t = 0 ↔ Disjoint s t
Full source
theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinterndinter s t = 0 ↔ Disjoint s t := by
rw [← subset_zero]; simp [subset_iff, disjoint_left]Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the non-multiplicity-preserving intersection `ndinter s t` equals the empty multiset $0$ if and only if $s$ and $t$ are disjoint. In other words, $s$ and $t$ have no common elements (with nonzero multiplicity).
Multiset.Subset.ndinter_eq_left
theorem
{s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s
Full source
theorem Subset.ndinter_eq_left {s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s := by
induction s, t using Quot.induction_on₂
rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, if $s$ is a subset of $t$, then the non-multiplicity-preserving intersection of $s$ and $t$ equals $s$, i.e., $s \cap t = s$.