List.cons_bagInter_of_pos
theorem List.cons_bagInter_of_pos :
∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
a ∈ l₂ → (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
This theorem, `List.cons_bagInter_of_pos`, states that for any type `α` with decidable equality (`DecidableEq α`) and for any initial list `l₂`, any element `a : α` and another list `l₁`, if `a` is a member of `l₂`, then the multiset intersection (`List.bagInter`) of the list with `a` as the head and `l₁` as the tail (`a :: l₁`) with `l₂` equals to a list with `a` as the head and the multiset intersection of `l₁` and `l₂` with `a` erased as the tail (`a :: List.bagInter l₁ (List.erase l₂ a)`). In other words, when `a` is in `l₂`, `a` will also be in the multiset intersection of `(a :: l₁)` and `l₂`, and the remaining intersection is just the multiset intersection of `l₁` and `l₂` without `a`.
More concisely: For lists `l₁` and `l₂` over a type `α` with decidable equality, if `a` is an element of `l₂`, then `a :: List.bagInter l₁ l₂` equals `a :: List.bagInter l₁ (List.erase l₂ a)`.
|
List.nil_bagInter
theorem List.nil_bagInter : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), [].bagInter l = []
The theorem `List.nil_bagInter` states that for any type `α` that has a decidable equality and for any list `l` of type `α`, the bag intersection of an empty list with `l` is an empty list. Here, a bag intersection is a concept similar to the intersection of two sets, but it applies to lists (or "bags") and takes into account the multiplicity of elements.
More concisely: For any type `α` with decidable equality and any list `l` of type `α`, the bag intersection of the empty list with `l` is the empty list.
|
List.cons_bagInter_of_neg
theorem List.cons_bagInter_of_neg :
∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
a ∉ l₂ → (a :: l₁).bagInter l₂ = l₁.bagInter l₂
The theorem `List.cons_bagInter_of_neg` asserts that for any type `α`, a list `l₂` of type `α`, an element `a` of type `α`, and any instance of decidable equality on `α` (which allows us to decide if two elements of `α` are equal), given a list `l₁` of type `α`, if `a` is not in `l₂`, then the bag intersection of the list `l₂` with the list that has `a` as its head and `l₁` as its tail, is equal to the bag intersection of `l₁` with `l₂`.
In simpler terms, it states that if an element `a` is not in a list `l₂`, then `a` does not affect the common elements between `l₂` and any list that includes `a` and `l₁`.
More concisely: If `α` has decidable equality and `a ∉ l₂`, then `bagInter (cons α a l₁) l₂ = bagInter l₁ l₂`.
|