Mathlib.Data.List.Lattice

List.Disjoint.symm theorem

(d : Disjoint l₁ l₂) : Disjoint l₂ l₁

Full source

@[symm]
theorem Disjoint.symm (d : Disjoint l₁ l₂) : Disjoint l₂ l₁ := fun _ i₂ i₁ => d i₁ i₂

Symmetry of List Disjointness

Informal description

For any two lists `l₁` and `l₂`, if they are disjoint (i.e., `Disjoint l₁ l₂`), then they are also disjoint in the reverse order (i.e., `Disjoint l₂ l₁`).

List.mem_union_left theorem

(h : a ∈ l₁) (l₂ : List α) : a ∈ l₁ ∪ l₂

Full source

theorem mem_union_left (h : a ∈ l₁) (l₂ : List α) : a ∈ l₁ ∪ l₂ :=
  mem_union_iff.2 (Or.inl h)

Element in Left List is in Union

Informal description

For any element $a$ in a list $l₁$ and for any list $l₂$, the element $a$ is also in the union list $l₁ \cup l₂$.

List.mem_union_right theorem

(l₁ : List α) (h : a ∈ l₂) : a ∈ l₁ ∪ l₂

Full source

theorem mem_union_right (l₁ : List α) (h : a ∈ l₂) : a ∈ l₁ ∪ l₂ :=
  mem_union_iff.2 (Or.inr h)

Membership Preservation in List Union (Right)

Informal description

For any list `l₁` of type `α` and any element `a` that belongs to another list `l₂`, the element `a` is also a member of the union `l₁ ∪ l₂`.

List.sublist_suffix_of_union theorem

: ∀ l₁ l₂ : List α, ∃ t, t <+ l₁ ∧ t ++ l₂ = l₁ ∪ l₂

Full source

theorem sublist_suffix_of_union : ∀ l₁ l₂ : List α, ∃ t, t <+ l₁ ∧ t ++ l₂ = l₁ ∪ l₂
  | [], _ => ⟨[], by rfl, rfl⟩
  | a :: l₁, l₂ =>
    let ⟨t, s, e⟩ := sublist_suffix_of_union l₁ l₂
    if h : a ∈ l₁ ∪ l₂ then
      ⟨t, sublist_cons_of_sublist _ s, by
        simp only [e, cons_union, insert_of_mem h]⟩
    else
      ⟨a :: t, s.cons_cons _, by
        simp only [cons_append, cons_union, e, insert_of_not_mem h]⟩

Existence of Sublist Suffix for List Union

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, there exists a sublist $t$ of $l₁$ such that $t$ is a suffix of $l₁$ and the concatenation of $t$ with $l₂$ equals the union $l₁ \cup l₂$.

List.suffix_union_right theorem

(l₁ l₂ : List α) : l₂ <:+ l₁ ∪ l₂

Full source

theorem suffix_union_right (l₁ l₂ : List α) : l₂ <:+ l₁ ∪ l₂ :=
  (sublist_suffix_of_union l₁ l₂).imp fun _ => And.right

Right List is Suffix of Union

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the list $l_2$ is a suffix of the union $l_1 \cup l_2$.

List.union_sublist_append theorem

(l₁ l₂ : List α) : l₁ ∪ l₂ <+ l₁ ++ l₂

Full source

theorem union_sublist_append (l₁ l₂ : List α) : l₁ ∪ l₂l₁ ∪ l₂ <+ l₁ ++ l₂ :=
  let ⟨_, s, e⟩ := sublist_suffix_of_union l₁ l₂
  e ▸ (append_sublist_append_right _).2 s

Union Sublist of Concatenation

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the union $l_1 \cup l_2$ is a sublist of the concatenation $l_1 ++ l_2$.

List.forall_mem_union theorem

: (∀ x ∈ l₁ ∪ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ ∀ x ∈ l₂, p x

Full source

theorem forall_mem_union : (∀ x ∈ l₁ ∪ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ ∀ x ∈ l₂, p x := by
  simp only [mem_union_iff, or_imp, forall_and]

Universal Quantification over List Union

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, and any predicate $p$ on $\alpha$, the following are equivalent: 1. For all $x$ in the union $l₁ ∪ l₂$, $p(x)$ holds 2. For all $x$ in $l₁$, $p(x)$ holds, and for all $x$ in $l₂$, $p(x)$ holds

List.forall_mem_of_forall_mem_union_left theorem

(h : ∀ x ∈ l₁ ∪ l₂, p x) : ∀ x ∈ l₁, p x

Full source

theorem forall_mem_of_forall_mem_union_left (h : ∀ x ∈ l₁ ∪ l₂, p x) : ∀ x ∈ l₁, p x :=
  (forall_mem_union.1 h).1

Universal Property of List Union (Left Factor)

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, and any predicate $p$ on $\alpha$, if $p(x)$ holds for all $x$ in the union $l_1 \cup l_2$, then $p(x)$ holds for all $x$ in $l_1$.

List.forall_mem_of_forall_mem_union_right theorem

(h : ∀ x ∈ l₁ ∪ l₂, p x) : ∀ x ∈ l₂, p x

Full source

theorem forall_mem_of_forall_mem_union_right (h : ∀ x ∈ l₁ ∪ l₂, p x) : ∀ x ∈ l₂, p x :=
  (forall_mem_union.1 h).2

Universal Quantification over List Union Implies Right List

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, and any predicate $p$ on $\alpha$, if $p(x)$ holds for all $x$ in the union $l₁ ∪ l₂$, then $p(x)$ holds for all $x$ in $l₂$.

List.Subset.union_eq_right theorem

{xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys

Full source

theorem Subset.union_eq_right {xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]

Union with Superset Equals Superset for Lists

Informal description

For any lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a subset of $ys$ (i.e., every element of $xs$ appears in $ys$), then the union $xs \cup ys$ equals $ys$.

List.inter_nil theorem

(l : List α) : [] ∩ l = []

Full source

@[simp]
theorem inter_nil (l : List α) : [][] ∩ l = [] :=
  rfl

Empty List Intersection Property

Informal description

For any list $l$ of elements of type $\alpha$, the intersection of the empty list `[]` with $l$ is the empty list, i.e., $[] \cap l = []$.

List.inter_cons_of_mem theorem

(l₁ : List α) (h : a ∈ l₂) : (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Full source

@[simp]
theorem inter_cons_of_mem (l₁ : List α) (h : a ∈ l₂) : (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂ := by
  simp [Inter.inter, List.inter, h]

Cons Preservation in List Intersection for Present Elements

Informal description

For any list $l_1$ and element $a$ such that $a \in l_2$, the intersection of the list $a :: l_1$ with $l_2$ is equal to $a$ prepended to the intersection of $l_1$ with $l_2$. In other words, $(a :: l_1) \cap l_2 = a :: (l_1 \cap l_2)$.

List.inter_cons_of_not_mem theorem

(l₁ : List α) (h : a ∉ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Full source

@[simp]
theorem inter_cons_of_not_mem (l₁ : List α) (h : a ∉ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂ := by
  simp [Inter.inter, List.inter, h]

Intersection with Cons Element Not in Second List

Informal description

For any list $l_1$ of elements of type $\alpha$ and an element $a \notin l_2$, the intersection of the list $a :: l_1$ with $l_2$ is equal to the intersection of $l_1$ with $l_2$, i.e., $(a :: l_1) \cap l_2 = l_1 \cap l_2$.

List.inter_nil' theorem

(l : List α) : l ∩ [] = []

Full source

@[simp]
theorem inter_nil' (l : List α) : l ∩ [] = [] := by
  induction l with
  | nil => rfl
  | cons x xs ih => by_cases x ∈ xs <;> simp [ih]

Intersection with Empty List Yields Empty List

Informal description

For any list $l$ of elements of type $\alpha$, the intersection of $l$ with the empty list is the empty list, i.e., $l \cap [] = []$.

List.mem_of_mem_inter_left theorem

: a ∈ l₁ ∩ l₂ → a ∈ l₁

Full source

theorem mem_of_mem_inter_left : a ∈ l₁ ∩ l₂ → a ∈ l₁ :=
  mem_of_mem_filter

Element in List Intersection Implies Element in First List

Informal description

For any element $a$ and lists $l₁$ and $l₂$, if $a$ belongs to the intersection $l₁ ∩ l₂$, then $a$ belongs to $l₁$.

List.mem_of_mem_inter_right theorem

(h : a ∈ l₁ ∩ l₂) : a ∈ l₂

Full source

theorem mem_of_mem_inter_right (h : a ∈ l₁ ∩ l₂) : a ∈ l₂ := by simpa using of_mem_filter h

Element in List Intersection Implies Element in Right Operand

Informal description

For any element $a$ and lists $l_1$ and $l_2$, if $a$ is in the intersection $l_1 \cap l_2$, then $a$ is in $l_2$.

List.mem_inter_of_mem_of_mem theorem

(h₁ : a ∈ l₁) (h₂ : a ∈ l₂) : a ∈ l₁ ∩ l₂

Full source

theorem mem_inter_of_mem_of_mem (h₁ : a ∈ l₁) (h₂ : a ∈ l₂) : a ∈ l₁ ∩ l₂ :=
  mem_filter_of_mem h₁ <| by simpa using h₂

Membership in List Intersection from Membership in Both Lists

Informal description

For any element $a$ and lists $l₁$ and $l₂$, if $a$ belongs to $l₁$ and $a$ belongs to $l₂$, then $a$ belongs to the intersection $l₁ ∩ l₂$.

List.inter_subset_left theorem

{l₁ l₂ : List α} : l₁ ∩ l₂ ⊆ l₁

Full source

theorem inter_subset_left {l₁ l₂ : List α} : l₁ ∩ l₂l₁ ∩ l₂ ⊆ l₁ :=
  filter_subset' _

Intersection is Subset of First List

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the intersection $l₁ ∩ l₂$ is a subset of $l₁$.

List.inter_subset_right theorem

{l₁ l₂ : List α} : l₁ ∩ l₂ ⊆ l₂

Full source

theorem inter_subset_right {l₁ l₂ : List α} : l₁ ∩ l₂l₁ ∩ l₂ ⊆ l₂ := fun _ => mem_of_mem_inter_right

Intersection is Subset of Second List

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the intersection $l_1 \cap l_2$ is a subset of $l_2$.

List.subset_inter theorem

{l l₁ l₂ : List α} (h₁ : l ⊆ l₁) (h₂ : l ⊆ l₂) : l ⊆ l₁ ∩ l₂

Full source

theorem subset_inter {l l₁ l₂ : List α} (h₁ : l ⊆ l₁) (h₂ : l ⊆ l₂) : l ⊆ l₁ ∩ l₂ := fun _ h =>
  mem_inter_iff.2 ⟨h₁ h, h₂ h⟩

Subset Preservation Under List Intersection

Informal description

For any lists $l$, $l_1$, and $l_2$ of elements of type $\alpha$, if $l$ is a subset of $l_1$ and $l$ is a subset of $l_2$, then $l$ is a subset of the intersection $l_1 \cap l_2$.

List.inter_eq_nil_iff_disjoint theorem

: l₁ ∩ l₂ = [] ↔ Disjoint l₁ l₂

Full source

theorem inter_eq_nil_iff_disjoint : l₁ ∩ l₂l₁ ∩ l₂ = [] ↔ Disjoint l₁ l₂ := by
  simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]
  rfl

Empty Intersection Characterizes Disjoint Lists

Informal description

For any two lists `l₁` and `l₂`, their intersection `l₁ ∩ l₂` is empty if and only if they are disjoint (i.e., they share no common elements).

List.forall_mem_inter_of_forall_left theorem

(h : ∀ x ∈ l₁, p x) (l₂ : List α) : ∀ x, x ∈ l₁ ∩ l₂ → p x

Full source

theorem forall_mem_inter_of_forall_left (h : ∀ x ∈ l₁, p x) (l₂ : List α) :
    ∀ x, x ∈ l₁ ∩ l₂ → p x :=
  BAll.imp_left (fun _ => mem_of_mem_inter_left) h

Preservation of Predicate over List Intersection from Left List

Informal description

For any predicate $p$ and lists $l₁$ and $l₂$ of elements of type $\alpha$, if $p(x)$ holds for all $x \in l₁$, then $p(x)$ also holds for all $x$ in the intersection $l₁ ∩ l₂$.

List.forall_mem_inter_of_forall_right theorem

(l₁ : List α) (h : ∀ x ∈ l₂, p x) : ∀ x, x ∈ l₁ ∩ l₂ → p x

Full source

theorem forall_mem_inter_of_forall_right (l₁ : List α) (h : ∀ x ∈ l₂, p x) :
    ∀ x, x ∈ l₁ ∩ l₂ → p x :=
  BAll.imp_left (fun _ => mem_of_mem_inter_right) h

Predicate Preservation in List Intersection from Right Operand

Informal description

For any list $l_1$ of elements of type $\alpha$, if a predicate $p$ holds for all elements in another list $l_2$, then $p$ holds for all elements in the intersection $l_1 \cap l_2$.

List.inter_reverse theorem

{xs ys : List α} : xs.inter ys.reverse = xs.inter ys

Full source

@[simp]
theorem inter_reverse {xs ys : List α} : xs.inter ys.reverse = xs.inter ys := by
  simp only [List.inter, elem_eq_mem, mem_reverse]

Intersection Invariance Under List Reversal

Informal description

For any two lists `xs` and `ys` of elements of type `α`, the intersection of `xs` with the reverse of `ys` is equal to the intersection of `xs` with `ys`. In other words, reversing the second list does not affect the intersection result: $$ \text{xs} \cap \text{ys.reverse} = \text{xs} \cap \text{ys} $$

List.Subset.inter_eq_left theorem

{xs ys : List α} (h : xs ⊆ ys) : xs ∩ ys = xs

Full source

theorem Subset.inter_eq_left {xs ys : List α} (h : xs ⊆ ys) : xs ∩ ys = xs :=
  List.filter_eq_self.mpr fun _ ha => elem_eq_true_of_mem (h ha)

Intersection of Subset Lists Equals the Subset List

Informal description

For any two lists `xs` and `ys` of elements of type `α`, if `xs` is a subset of `ys`, then the intersection of `xs` and `ys` is equal to `xs`. In other words, if every element of `xs` appears in `ys`, then `xs ∩ ys = xs`.

List.nil_bagInter theorem

(l : List α) : [].bagInter l = []

Full source

@[simp]
theorem nil_bagInter (l : List α) : [].bagInter l = [] := by cases l <;> rfl

Empty List Bag Intersection Property

Informal description

For any list $l$ of elements of type $\alpha$, the bag intersection of the empty list with $l$ is the empty list, i.e., $[\,] \cap_{\text{bag}} l = [\,]$.

List.bagInter_nil theorem

(l : List α) : l.bagInter [] = []

Full source

@[simp]
theorem bagInter_nil (l : List α) : l.bagInter [] = [] := by cases l <;> rfl

Bag Intersection with Empty List Yields Empty List

Informal description

For any list $l$ of elements of type $\alpha$, the bag intersection of $l$ with the empty list is the empty list, i.e., $l \cap_{\text{bag}} [\,] = [\,]$.

List.cons_bagInter_of_pos theorem

(l₁ : List α) (h : a ∈ l₂) : (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Full source

@[simp]
theorem cons_bagInter_of_pos (l₁ : List α) (h : a ∈ l₂) :
    (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a) := by
  cases l₂
  · exact if_pos h
  · simp only [List.bagInter, if_pos (elem_eq_true_of_mem h)]

Bag Intersection with Cons Element When Present in Second List

Informal description

For any list $l₁$ of elements of type $\alpha$ and any element $a$ that is a member of list $l₂$, the bag intersection of the list $a :: l₁$ with $l₂$ is equal to $a$ followed by the bag intersection of $l₁$ with the list obtained by removing one occurrence of $a$ from $l₂$. In other words, $(a :: l₁) \cap_{\text{bag}} l₂ = a :: (l₁ \cap_{\text{bag}} (l₂ \setminus \{a\}))$.

List.cons_bagInter_of_neg theorem

(l₁ : List α) (h : a ∉ l₂) : (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Full source

@[simp]
theorem cons_bagInter_of_neg (l₁ : List α) (h : a ∉ l₂) :
    (a :: l₁).bagInter l₂ = l₁.bagInter l₂ := by
  cases l₂; · simp only [bagInter_nil]
  simp only [erase_of_not_mem h, List.bagInter, if_neg (mt mem_of_elem_eq_true h)]

Bag Intersection with Cons Element When Absent from Second List

Informal description

For any list $l₁$ of elements of type $\alpha$ and any element $a$ that is not a member of list $l₂$, the bag intersection of the list $a :: l₁$ with $l₂$ is equal to the bag intersection of $l₁$ with $l₂$. In other words, $(a :: l₁) \cap_{\text{bag}} l₂ = l₁ \cap_{\text{bag}} l₂$.

List.mem_bagInter theorem

{a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Full source

@[simp]
theorem mem_bagInter {a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁.bagInter l₂a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
  | [], l₂ => by simp only [nil_bagInter, not_mem_nil, false_and]
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂
    · rw [cons_bagInter_of_pos _ h, mem_cons, mem_cons, mem_bagInter]
      by_cases ba : a = b
      · simp only [ba, h, eq_self_iff_true, true_or, true_and]
      · simp only [mem_erase_of_ne ba, ba, false_or]
    · rw [cons_bagInter_of_neg _ h, mem_bagInter, mem_cons, or_and_right]
      symm
      apply or_iff_right_of_imp
      rintro ⟨rfl, h'⟩
      exact h.elim h'

Membership in Bag Intersection is Equivalent to Membership in Both Lists

Informal description

For any element $a$ of type $\alpha$ and any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the element $a$ belongs to the bag intersection $l₁ \cap_{\text{bag}} l₂$ if and only if $a$ belongs to both $l₁$ and $l₂$. In other words, \[ a \in l₁ \cap_{\text{bag}} l₂ \leftrightarrow a \in l₁ \land a \in l₂. \]

List.count_bagInter theorem

{a : α} : ∀ {l₁ l₂ : List α}, count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)

Full source

@[simp]
theorem count_bagInter {a : α} :
    ∀ {l₁ l₂ : List α}, count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
  | [], l₂ => by simp
  | l₁, [] => by simp
  | b :: l₁, l₂ => by
    by_cases hb : b ∈ l₂
    · rw [cons_bagInter_of_pos _ hb, count_cons, count_cons, count_bagInter, count_erase,
        ← Nat.add_min_add_right]
      by_cases ba : b = a
      · simp only [beq_iff_eq]
        rw [if_pos ba, Nat.sub_add_cancel]
        rwa [succ_le_iff, count_pos_iff, ← ba]
      · simp only [beq_iff_eq]
        rw [if_neg ba, Nat.sub_zero, Nat.add_zero, Nat.add_zero]
    · rw [cons_bagInter_of_neg _ hb, count_bagInter]
      by_cases ab : a = b
      · rw [← ab] at hb
        rw [count_eq_zero.2 hb, Nat.min_zero, Nat.min_zero]
      · rw [count_cons_of_ne (Ne.symm ab)]

Count in Bag Intersection Equals Minimum of Counts

Informal description

For any element $a$ of type $\alpha$ and any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the count of $a$ in the bag intersection of $l₁$ and $l₂$ is equal to the minimum of the counts of $a$ in $l₁$ and $l₂$. That is, \[ \text{count}(a, l₁ \cap_{\text{bag}} l₂) = \min(\text{count}(a, l₁), \text{count}(a, l₂)). \]

List.bagInter_sublist_left theorem

: ∀ l₁ l₂ : List α, l₁.bagInter l₂ <+ l₁

Full source

theorem bagInter_sublist_left : ∀ l₁ l₂ : List α, l₁.bagInter l₂ <+ l₁
  | [], l₂ => by simp
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂ <;> simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
    · exact (bagInter_sublist_left _ _).cons_cons _
    · apply sublist_cons_of_sublist
      apply bagInter_sublist_left

Sublist Property of Bag Intersection: $l₁ \cap_{\text{bag}} l₂$ is a sublist of $l₁$

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the bag intersection $l₁ \cap_{\text{bag}} l₂$ is a sublist of $l₁$. In other words, all elements of $l₁ \cap_{\text{bag}} l₂$ appear in $l₁$ in the same order, though not necessarily consecutively.

List.bagInter_nil_iff_inter_nil theorem

: ∀ l₁ l₂ : List α, l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []

Full source

theorem bagInter_nil_iff_inter_nil : ∀ l₁ l₂ : List α, l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
  | [], l₂ => by simp
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂
    · simp [h]
    · simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

Empty Bag Intersection iff Empty Regular Intersection

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the bag intersection $l₁ \cap_{\text{bag}} l₂$ is empty if and only if the intersection $l₁ \cap l₂$ is empty. In other words, $l₁ \cap_{\text{bag}} l₂ = [\,] \leftrightarrow l₁ \cap l₂ = [\,]$.