mathlib3 documentation

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 α) :

list.nil.disjoint l

@[simp]

theorem list.disjoint_nil_right {α : Type u_1} (l : list α) :

l.disjoint list.nil

@[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) :

(list.take m l).disjoint (list.drop n l)

`union` #

@[simp]

theorem list.nil_union {α : Type u_1} [decidable_eq α] (l : list α) :

list.nil ∪ l = l

@[simp]

theorem list.cons_union {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) (a : α) :

a :: l₁ ∪ l₂ = has_insert.insert a (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 α) :

list.nil ∩ l = list.nil

@[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 α) :

list.nil.bag_inter l = list.nil

@[simp]

theorem list.bag_inter_nil {α : Type u_1} [decidable_eq α] (l : list α) :

l.bag_inter list.nil = list.nil

@[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 α} :

list.count a (l₁.bag_inter l₂) = linear_order.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