Lattice structure of lists

This files prove 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₁ : List α} {l₂ : List α} (d : List.Disjoint l₁ l₂) : List.Disjoint l₂ 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₁ : List α) (l₂ : List α) : ∃ (t : List α), List.Sublist t l₁ ∧ t ++ l₂ = l₁ ∪ l₂

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

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

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

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_not_mem {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : ¬a ∈ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂

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

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

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

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

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

theorem List.subset_inter {α : Type u_1} [DecidableEq α] {l : List α} {l₁ : List α} {l₂ : List α} (h₁ : l ⊆ l₁) (h₂ : l ⊆ l₂) : l ⊆ l₁ ∩ l₂

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

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 : List α} {ys : List α} : List.inter xs (List.reverse ys) = List.inter xs ys

bagInter

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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