# mathlib3documentation

data.list.lattice

# Lattice structure of lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files prove basic properties about list.disjoint, list.union, list.inter and list.bag_inter, which are defined in core Lean and data.list.defs.

l₁ ∪ l₂ is the list where all elements of l₁ have been inserted in l₂ in order. For example, [0, 0, 1, 2, 2, 3] ∪ [4, 3, 3, 0] = [1, 2, 4, 3, 3, 0]

l₁ ∩ l₂ is the list of elements of l₁ in order which are in l₂. For example, [0, 0, 1, 2, 2, 3] ∪ [4, 3, 3, 0] = [0, 0, 3]

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₁. As opposed to list.inter, list.bag_inter copes well with multiplicity. For example, bag_inter [0, 1, 2, 3, 2, 1, 0] [1, 0, 1, 4, 3] = [0, 1, 3, 1]

### disjoint#

theorem list.disjoint.symm {α : Type u_1} {l₁ l₂ : list α} (d : l₁.disjoint l₂) :
l₂.disjoint l₁
theorem list.disjoint_comm {α : Type u_1} {l₁ l₂ : list α} :
l₁.disjoint l₂ l₂.disjoint l₁
theorem list.disjoint_left {α : Type u_1} {l₁ l₂ : list α} :
l₁.disjoint l₂ ⦃a : α⦄, a l₁ a l₂
theorem list.disjoint_right {α : Type u_1} {l₁ l₂ : list α} :
l₁.disjoint l₂ ⦃a : α⦄, a l₂ a l₁
theorem list.disjoint_iff_ne {α : Type u_1} {l₁ l₂ : list α} :
l₁.disjoint l₂ (a : α), a l₁ (b : α), b l₂ a b
theorem list.disjoint_of_subset_left {α : Type u_1} {l l₁ l₂ : list α} (ss : l₁ l) (d : l.disjoint l₂) :
l₁.disjoint l₂
theorem list.disjoint_of_subset_right {α : Type u_1} {l l₁ l₂ : list α} (ss : l₂ l) (d : l₁.disjoint l) :
l₁.disjoint l₂
theorem list.disjoint_of_disjoint_cons_left {α : Type u_1} {a : α} {l₁ l₂ : list α} :
(a :: l₁).disjoint l₂ l₁.disjoint l₂
theorem list.disjoint_of_disjoint_cons_right {α : Type u_1} {a : α} {l₁ l₂ : list α} :
l₁.disjoint (a :: l₂) l₁.disjoint l₂
@[simp]
theorem list.disjoint_nil_left {α : Type u_1} (l : list α) :
@[simp]
theorem list.disjoint_nil_right {α : Type u_1} (l : list α) :
@[simp]
theorem list.singleton_disjoint {α : Type u_1} {l : list α} {a : α} :
[a].disjoint l a l
@[simp]
theorem list.disjoint_singleton {α : Type u_1} {l : list α} {a : α} :
l.disjoint [a] a l
@[simp]
theorem list.disjoint_append_left {α : Type u_1} {l l₁ l₂ : list α} :
(l₁ ++ l₂).disjoint l l₁.disjoint l l₂.disjoint l
@[simp]
theorem list.disjoint_append_right {α : Type u_1} {l l₁ l₂ : list α} :
l.disjoint (l₁ ++ l₂) l.disjoint l₁ l.disjoint l₂
@[simp]
theorem list.disjoint_cons_left {α : Type u_1} {l₁ l₂ : list α} {a : α} :
(a :: l₁).disjoint l₂ a l₂ l₁.disjoint l₂
@[simp]
theorem list.disjoint_cons_right {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁.disjoint (a :: l₂) a l₁ l₁.disjoint l₂
theorem list.disjoint_of_disjoint_append_left_left {α : Type u_1} {l l₁ l₂ : list α} (d : (l₁ ++ l₂).disjoint l) :
l₁.disjoint l
theorem list.disjoint_of_disjoint_append_left_right {α : Type u_1} {l l₁ l₂ : list α} (d : (l₁ ++ l₂).disjoint l) :
l₂.disjoint l
theorem list.disjoint_of_disjoint_append_right_left {α : Type u_1} {l l₁ l₂ : list α} (d : l.disjoint (l₁ ++ l₂)) :
l.disjoint l₁
theorem list.disjoint_of_disjoint_append_right_right {α : Type u_1} {l l₁ l₂ : list α} (d : l.disjoint (l₁ ++ l₂)) :
l.disjoint l₂
theorem list.disjoint_take_drop {α : Type u_1} {l : list α} {m n : } (hl : l.nodup) (h : m n) :
l).disjoint l)

### union#

@[simp]
theorem list.nil_union {α : Type u_1} [decidable_eq α] (l : list α) :
= l
@[simp]
theorem list.cons_union {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) (a : α) :
a :: l₁ l₂ = (l₁ l₂)
@[simp]
theorem list.mem_union {α : Type u_1} {l₁ l₂ : list α} {a : α} [decidable_eq α] :
a l₁ l₂ a l₁ a l₂
theorem list.mem_union_left {α : Type u_1} {l₁ : list α} {a : α} [decidable_eq α] (h : a l₁) (l₂ : list α) :
a l₁ l₂
theorem list.mem_union_right {α : Type u_1} {l₂ : list α} {a : α} [decidable_eq α] (l₁ : list α) (h : a l₂) :
a l₁ l₂
theorem list.sublist_suffix_of_union {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
(t : list α), t <+ l₁ t ++ l₂ = l₁ l₂
theorem list.suffix_union_right {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
l₂ <:+ l₁ l₂
theorem list.union_sublist_append {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
l₁ l₂ <+ l₁ ++ l₂
theorem list.forall_mem_union {α : Type u_1} {l₁ l₂ : list α} {p : α Prop} [decidable_eq α] :
( (x : α), x l₁ l₂ p x) ( (x : α), x l₁ p x) (x : α), x l₂ p x
theorem list.forall_mem_of_forall_mem_union_left {α : Type u_1} {l₁ l₂ : list α} {p : α Prop} [decidable_eq α] (h : (x : α), x l₁ l₂ p x) (x : α) (H : x l₁) :
p x
theorem list.forall_mem_of_forall_mem_union_right {α : Type u_1} {l₁ l₂ : list α} {p : α Prop} [decidable_eq α] (h : (x : α), x l₁ l₂ p x) (x : α) (H : x l₂) :
p x

### inter#

@[simp]
theorem list.inter_nil {α : Type u_1} [decidable_eq α] (l : list α) :
@[simp]
theorem list.inter_cons_of_mem {α : Type u_1} {l₂ : list α} {a : α} [decidable_eq α] (l₁ : list α) (h : a l₂) :
(a :: l₁) l₂ = a :: l₁ l₂
@[simp]
theorem list.inter_cons_of_not_mem {α : Type u_1} {l₂ : list α} {a : α} [decidable_eq α] (l₁ : list α) (h : a l₂) :
(a :: l₁) l₂ = l₁ l₂
theorem list.mem_of_mem_inter_left {α : Type u_1} {l₁ l₂ : list α} {a : α} [decidable_eq α] :
a l₁ l₂ a l₁
theorem list.mem_of_mem_inter_right {α : Type u_1} {l₁ l₂ : list α} {a : α} [decidable_eq α] :
a l₁ l₂ a l₂
theorem list.mem_inter_of_mem_of_mem {α : Type u_1} {l₁ l₂ : list α} {a : α} [decidable_eq α] :
a l₁ a l₂ a l₁ l₂
@[simp]
theorem list.mem_inter {α : Type u_1} {l₁ l₂ : list α} {a : α} [decidable_eq α] :
a l₁ l₂ a l₁ a l₂
theorem list.inter_subset_left {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
l₁ l₂ l₁
theorem list.inter_subset_right {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
l₁ l₂ l₂
theorem list.subset_inter {α : Type u_1} [decidable_eq α] {l l₁ l₂ : list α} (h₁ : l l₁) (h₂ : l l₂) :
l l₁ l₂
theorem list.inter_eq_nil_iff_disjoint {α : Type u_1} {l₁ l₂ : list α} [decidable_eq α] :
l₁ l₂ = list.nil l₁.disjoint l₂
theorem list.forall_mem_inter_of_forall_left {α : Type u_1} {l₁ : list α} {p : α Prop} [decidable_eq α] (h : (x : α), x l₁ p x) (l₂ : list α) (x : α) :
x l₁ l₂ p x
theorem list.forall_mem_inter_of_forall_right {α : Type u_1} {l₂ : list α} {p : α Prop} [decidable_eq α] (l₁ : list α) (h : (x : α), x l₂ p x) (x : α) :
x l₁ l₂ p x
@[simp]
theorem list.inter_reverse {α : Type u_1} [decidable_eq α] {xs ys : list α} :
xs.inter ys.reverse = xs.inter ys

### bag_inter#

@[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} {l₂ : list α} {a : α} [decidable_eq α] (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} {l₂ : list α} {a : α} [decidable_eq α] (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 α} :
(l₁.bag_inter l₂) = linear_order.min l₁) 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