Multiset.mem_ndunion
theorem Multiset.mem_ndunion :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, a ∈ s.ndunion t ↔ a ∈ s ∨ a ∈ t
This theorem states that for any type `α` with decidable equality and any elements `s`, `t` of type `Multiset α`, and any element `a` of type `α`, `a` is a member of the non-duplicate union of `s` and `t` if and only if `a` is a member of `s` or `a` is a member of `t`. This non-duplicate union operation, `Multiset.ndunion`, is a union operation on multisets that does not take into account multiplicities of elements. In other words, an element is included in the union set regardless of how many times it appears in the original sets.
More concisely: For any type `α` with decidable equality, and `s`, `t` multisets of `α`, an element `a` is in the non-duplicate union `s ∪_\_ t` if and only if it is in `s` or in `t`.
|
Multiset.mem_ndinter
theorem Multiset.mem_ndinter :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t
This theorem states that for any type `α` that has decidable equality, and for any multiset `s`, multiset `t`, and for an element `a` of type `α`, `a` is in the intersection of multisets `s` and `t` if and only if `a` is in `s` and `a` is in `t`. In other words, an element belongs to the intersection of two multisets if and only if it belongs to both of these multisets. The intersection here refers to the `ndinter` operation, which doesn't take into account the multiplicities of the elements.
More concisely: For any type `α` with decidable equality and multisets `s` and `t` over `α`, `a` is in the intersection of `s` and `t` if and only if `a` is in both `s` and `t`.
|
Mathlib.Data.Multiset.FinsetOps._auxLemma.1
theorem Mathlib.Data.Multiset.FinsetOps._auxLemma.1 :
∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, (a ∈ Multiset.ndinsert b s) = (a = b ∨ a ∈ s)
This theorem states that for any type `α` that has decidable equality, and for any elements `a` and `b` of type `α` and a multiset `s` of type `α`, `a` is in the multiset obtained by non-duplicate insertion of `b` into `s` if and only if `a` is equal to `b` or `a` is in `s`. In other words, an element `a` is in the multiset after the non-duplicate insertion of an element `b` if `a` is either the element inserted or was already in the multiset before the insertion.
More concisely: For any type `α` with decidable equality, and any multiset `s` of type `α` and elements `a, b` of type `α`, `a` is in the multiset `(s : set α) ++ {b}` if and only if `a = b` or `a` is in `s`.
|
Multiset.ndinsert_of_not_mem
theorem Multiset.ndinsert_of_not_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → Multiset.ndinsert a s = a ::ₘ s := by
sorry
This theorem states that for any type `α` with a decidable equality and any multiset `s` of this type, if an element `a` of type `α` is not a member of the multiset `s`, then using the `ndinsert` function to insert `a` into `s` will result in a new multiset where `a` is the first element followed by the elements of `s`. In terms of mathematical notation, if `a ∉ s`, then `ndinsert(a, s) = a :: s`. The `∉` symbol represents "not a member of" and `::` represents adding an element at the beginning of a list or a multiset.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, if `a notin s`, then `ndinsert(a, s) = a :: s`.
|
Mathlib.Data.Multiset.FinsetOps._auxLemma.5
theorem Mathlib.Data.Multiset.FinsetOps._auxLemma.5 :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, (a ∈ s.ndunion t) = (a ∈ s ∨ a ∈ t)
This theorem states that for any type `α` with decidable equality and any elements `s` and `t` of type `Multiset α` and any `a` of type `α`, `a` belongs to the non-duplicating union of `s` and `t` if and only if `a` belongs to `s` or `a` belongs to `t`. In other words, an element `a` is in the non-duplicating union of two multisets `s` and `t` exactly when it is in either `s` or `t`. This theorem basically presents the property of a set union in the context of multisets.
More concisely: For any type `α` with decidable equality, and multisets `s` and `t` of type `Multiset α`, the non-duplicating union of `s` and `t` equals the set of elements in `s` or `t`.
|
Multiset.le_ndinter
theorem Multiset.le_ndinter :
∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u
The theorem `Multiset.le_ndinter` states that for any type `α` with decidable equality and any three multiset objects `s`, `t`, and `u` of type `α`, `s` is a subset of the intersection of `t` and `u` (denoted as `Multiset.ndinter t u`) if and only if `s` is a subset of `t` and every element of `s` is also an element of `u`. Here, `Multiset.ndinter t u` represents the intersection of multisets `t` and `u`, but unlike the standard intersection operation, it does not take into account the multiplicities of elements. The symbol "⊆" is used to denote the subset relationship.
More concisely: For any type `α` with decidable equality and multisets `s`, `t`, and `u` of type `α`, `s ⊆ Multiset.ndinter t u` if and only if `s ⊆ t` and each element of `s` is an element of `u`.
|
Multiset.mem_ndinsert
theorem Multiset.mem_ndinsert :
∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, a ∈ Multiset.ndinsert b s ↔ a = b ∨ a ∈ s := by
sorry
This theorem states that for any type `α` with a decidable equality relation, and given any elements `a` and `b` of type `α` and a multiset `s` of type `α`, the element `a` belongs to the multiset resulting from non-duplicate inserting `b` into `s` if and only if `a` is equal to `b` or `a` already belongs to `s`. In other words, after you insert an element `b` into a multiset `s` using the non-duplicate insert operation, an element `a` is in the resulting multiset if `a` was either the element you inserted, or it was already in the original multiset.
More concisely: For any decidably equal type `α` and multisets `s` of `α`, an element `a` is in the multiset obtained by non-duplicate insertion of `b` into `s` if and only if `a` is equal to `b` or already in `s`.
|
Multiset.ndinsert_of_mem
theorem Multiset.ndinsert_of_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → Multiset.ndinsert a s = s
The theorem `Multiset.ndinsert_of_mem` states that for any type `α` that has decidable equality, and for any element `a` of type `α` and any multiset `s` of type `α`, if `a` is an element of `s`, then inserting `a` into `s` (without respecting multiplicities) results in the same multiset `s`. In other words, if `a` is already in `s`, inserting `a` into `s` again will not change `s`.
More concisely: If `α` has decidable equality and `a` is an element of multiset `s` of type `α`, then `Multiset.ndinsert a s = s`.
|