mathlib documentation

data.list.bag_inter

source
@[simp]
theorem list.nil_bag_inter {α : Type u} [decidable_eq α] (l : list α) :
list.nil.bag_inter l = list.nil
source
@[simp]
theorem list.bag_inter_nil {α : Type u} [decidable_eq α] (l : list α) :
l.bag_inter list.nil = list.nil
source
@[simp]
theorem list.cons_bag_inter_of_pos {α : Type u} [decidable_eq α] {a : α} (l₁ : list α) {l₂ : list α} (h : a ∈ l₂) :
(a :: l₁).bag_inter l₂ = a :: l₁.bag_inter (l₂.erase a)
source
@[simp]
theorem list.cons_bag_inter_of_neg {α : Type u} [decidable_eq α] {a : α} (l₁ : list α) {l₂ : list α} (h : a ∉ l₂) :
(a :: l₁).bag_inter l₂ = l₁.bag_inter l₂
source
@[simp]
theorem list.mem_bag_inter {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
a ∈ l₁.bag_inter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
source
@[simp]
theorem list.count_bag_inter {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
list.count a (l₁.bag_inter l₂) = min (list.count a l₁) (list.count a l₂)
source
theorem list.bag_inter_sublist_left {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
l₁.bag_inter l₂ <+ l₁
source
theorem list.bag_inter_nil_iff_inter_nil {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
l₁.bag_inter l₂ = list.nil ↔ l₁ ∩ l₂ = list.nil