Documentation

Mathlib.Data.List.Lattice

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 : 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₁ : List α) (l₂ : List α) :
∃ (t : List α), t.Sublist 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 α) :
(l₁ l₂).Sublist (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
theorem List.Subset.union_eq_right {α : Type u_1} [DecidableEq α] {xs : List α} {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_not_mem {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : ¬a l₂) :
(a :: l₁) l₂ = 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₁ : 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₂ = [] l₁.Disjoint l₂
theorem List.Disjoint.inter_eq_nil {α : Type u_1} {l₁ : List α} {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 : List α} {ys : List α} :
xs.inter ys.reverse = xs.inter ys
theorem List.Subset.inter_eq_left {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (h : xs ys) :
xs ys = xs

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_pos {α : Type u_1} {l₂ : List α} {a : α} [DecidableEq α] (l₁ : List α) (h : a l₂) :
(a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
@[simp]
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₂
@[simp]
theorem List.mem_bagInter {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
a l₁.bagInter l₂ a l₁ a l₂
@[simp]
theorem List.count_bagInter {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
List.count a (l₁.bagInter l₂) = min (List.count a l₁) (List.count a l₂)
theorem List.bagInter_sublist_left {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
(l₁.bagInter l₂).Sublist l₁
theorem List.bagInter_nil_iff_inter_nil {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
l₁.bagInter l₂ = [] l₁ l₂ = []