# mathlibdocumentation

data.list.bag_inter

@[simp]
theorem list.nil_bag_inter {α : Type u} [decidable_eq α] (l : list α) :
@[simp]
theorem list.bag_inter_nil {α : Type u} [decidable_eq α] (l : list α) :
@[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)
@[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₂
@[simp]
theorem list.mem_bag_inter {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
a l₁.bag_inter l₂ a l₁ a l₂
@[simp]
theorem list.count_bag_inter {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
(l₁.bag_inter l₂) = min l₁) l₂)
theorem list.bag_inter_sublist_left {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
l₁.bag_inter l₂ <+ l₁
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