Lattice structure of lists

This file proves basic properties about List.disjoint, List.union, List.inter and List.bagInter, 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].

List.bagInter 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.bagInter copes well with multiplicity. For example, bagInter [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₁

union

theorem List.mem_union_left {α : Type u_1} {l₁ : List α} {a : α} [DecidableEq α] (h : a ∈ l₁) (l₂ : List α) : a ∈ l₁ ∪ l₂

theorem List.mem_union_right {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : a ∈ l₂) : a ∈ l₁ ∪ l₂

theorem List.sublist_suffix_of_union {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : ∃ (t : List α), t.Sublist l₁ ∧ t ++ l₂ = l₁ ∪ l₂

theorem List.suffix_union_right {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₂ <:+ l₁ ∪ l₂

theorem List.union_sublist_append {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : (l₁ ∪ l₂).Sublist (l₁ ++ l₂)

theorem List.forall_mem_union {α : Type u_1} {l₁ l₂ : List α} {p : α → Prop} [DecidableEq α] : (∀ (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} [DecidableEq α] (h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x) (x : α) : x ∈ l₁ → p x

theorem List.forall_mem_of_forall_mem_union_right {α : Type u_1} {l₁ l₂ : List α} {p : α → Prop} [DecidableEq α] (h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x) (x : α) : x ∈ l₂ → p x

theorem List.Subset.union_eq_right {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys

inter

@[simp]

theorem List.inter_nil {α : Type u_1} [DecidableEq α] (l : List α) : [] ∩ l = []

@[simp]

theorem List.inter_cons_of_mem {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : a ∈ l₂) : (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

@[simp]

theorem List.inter_cons_of_notMem {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : ¬a ∈ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂

theorem List.inter_cons {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) : (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂

@[simp]

theorem List.inter_nil' {α : Type u_1} [DecidableEq α] (l : List α) : l ∩ [] = []

theorem List.mem_of_mem_inter_left {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] : a ∈ l₁ ∩ l₂ → a ∈ l₁

theorem List.mem_of_mem_inter_right {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] (h : a ∈ l₁ ∩ l₂) : a ∈ l₂

theorem List.mem_inter_of_mem_of_mem {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] (h₁ : a ∈ l₁) (h₂ : a ∈ l₂) : a ∈ l₁ ∩ l₂

theorem List.inter_subset_left {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} : l₁ ∩ l₂ ⊆ l₁

theorem List.inter_subset_right {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} : l₁ ∩ l₂ ⊆ l₂

theorem List.subset_inter {α : Type u_1} [DecidableEq α] {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 α} [DecidableEq α] : l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂

theorem List.Disjoint.inter_eq_nil {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] : l₁.Disjoint l₂ → l₁ ∩ l₂ = []

Alias of the reverse direction of List.inter_eq_nil_iff_disjoint.

theorem List.forall_mem_inter_of_forall_left {α : Type u_1} {l₁ : List α} {p : α → Prop} [DecidableEq α] (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} [DecidableEq α] (l₁ : List α) (h : ∀ (x : α), x ∈ l₂ → p x) (x : α) : x ∈ l₁ ∩ l₂ → p x

@[simp]

theorem List.inter_reverse {α : Type u_1} [DecidableEq α] {xs ys : List α} : xs ∩ ys.reverse = xs ∩ ys

theorem List.Subset.inter_eq_left {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs ⊆ ys) : xs ∩ ys = xs

theorem List.Sublist.inter_left {α : Type u_1} [DecidableEq α] {l₁ l₂ l₃ : List α} (h : l₂.Sublist l₃) : (l₁ ∩ l₂).Sublist (l₁ ∩ l₃)

theorem List.Sublist.inter_right {α : Type u_1} [DecidableEq α] {l₁ l₂ l₃ : List α} (h : l₁.Sublist l₂) : (l₁ ∩ l₃).Sublist (l₂ ∩ l₃)

bagInter

@[simp]

theorem List.nil_bagInter {α : Type u_1} [DecidableEq α] (l : List α) : [].bagInter l = []

@[simp]

theorem List.bagInter_nil {α : Type u_1} [DecidableEq α] (l : List α) : l.bagInter [] = []

@[simp]

theorem List.cons_bagInter_of_mem {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : a ∈ l₂) : (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

@[deprecated List.cons_bagInter_of_mem (since := "2026-05-13")]

theorem List.cons_bagInter_of_pos {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : a ∈ l₂) : (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Alias of List.cons_bagInter_of_mem.

@[simp]

theorem List.cons_bagInter_of_not_mem {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : ¬a ∈ l₂) : (a :: l₁).bagInter l₂ = l₁.bagInter l₂

@[deprecated List.cons_bagInter_of_not_mem (since := "2026-05-13")]

theorem List.cons_bagInter_of_neg {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : ¬a ∈ l₂) : (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Alias of List.cons_bagInter_of_not_mem.

theorem List.cons_bagInter {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] : (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂

@[deprecated List.cons_bagInter (since := "2026-05-13")]

theorem List.cons_bagInteger {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] : (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂

Alias of List.cons_bagInter.

@[simp]

theorem List.bagInter_cons_of_not_mem {α : Type u_1} {l₁ : List α} {a : α} [DecidableEq α] (l₂ : List α) (h : ¬a ∈ l₁) : l₁.bagInter (a :: l₂) = l₁.bagInter l₂

@[simp]

theorem List.mem_bagInter {α : Type u_1} [DecidableEq α] {a : α} {l₁ l₂ : List α} : a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

@[simp]

theorem List.count_bagInter {α : Type u_1} [DecidableEq α] {a : α} {l₁ l₂ : List α} : count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)

theorem List.bagInter_sublist_left {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} : (l₁.bagInter l₂).Sublist l₁

theorem List.singleton_bagInter {α : Type u_1} {l₁ : List α} [DecidableEq α] (a : α) : [a].bagInter l₁ = if a ∈ l₁ then [a] else []

theorem List.bagInter_singleton {α : Type u_1} {l₁ : List α} [DecidableEq α] (a : α) : l₁.bagInter [a] = if a ∈ l₁ then [a] else []

@[simp]

theorem List.bagInter_erase_of_not_mem {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] (h : ¬a ∈ l₁) : l₁.bagInter (l₂.erase a) = l₁.bagInter l₂

@[simp]

theorem List.erase_bagInter_of_not_mem {α : Type u_1} {l₁ l₂ : List α} {a : α} [DecidableEq α] (h : ¬a ∈ l₂) : (l₁.erase a).bagInter l₂ = l₁.bagInter l₂

theorem List.bagInter_nil_iff_inter_nil {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []

@[simp]

theorem List.bagInter_eq_nil_iff_disjoint {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] : l₁.bagInter l₂ = [] ↔ l₁.Disjoint l₂

theorem List.Nodup.bagInter_right {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] (h : l₁.Nodup) : (l₁.bagInter l₂).Nodup

theorem List.Nodup.bagInter_left {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] (h : l₂.Nodup) : (l₁.bagInter l₂).Nodup

theorem List.Sublist.bagInter_inter {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] : (l₁.bagInter l₂).Sublist (l₁ ∩ l₂)