mathlib documentation

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 α} :
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 α} :
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 α} :
list.count a (l₁.bag_inter l₂) = min (list.count a l₁) (list.count a 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