mathlib documentation

data.list.bag_inter

List intersection #

This file provides basic results about list.bag_inter (definition in data.list.defs). bag_inter l₁ l₂ is the list of elements that are in both l₁ and l₂, counted with multiplicity and in the order they appear in l₁. For example, bag_inter [0, 1, 2, 3, 2, 1, 0] [1, 0, 1, 4, 3] = [0, 1, 3, 1]

@[simp]
theorem list.nil_bag_inter {α : Type u_1} [decidable_eq α] (l : list α) :
@[simp]
theorem list.bag_inter_nil {α : Type u_1} [decidable_eq α] (l : list α) :
@[simp]
theorem list.cons_bag_inter_of_pos {α : Type u_1} [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_1} [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_1} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
a l₁.bag_inter l₂ a l₁ a l₂
@[simp]
theorem list.count_bag_inter {α : Type u_1} [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_1} [decidable_eq α] (l₁ l₂ : list α) :
l₁.bag_inter l₂ <+ l₁
theorem list.bag_inter_nil_iff_inter_nil {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
l₁.bag_inter l₂ = list.nil l₁ l₂ = list.nil