List.Chain'.append_overlap
theorem List.Chain'.append_overlap :
∀ {α : Type u} {R : α → α → Prop} {l₁ l₂ l₃ : List α},
List.Chain' R (l₁ ++ l₂) → List.Chain' R (l₂ ++ l₃) → l₂ ≠ [] → List.Chain' R (l₁ ++ l₂ ++ l₃)
This theorem states that for any type `α` and binary relation `R` on `α`, given three lists `l₁`, `l₂`, and `l₃` of elements of type `α`, if the concatenated list `l₁ ++ l₂` and `l₂ ++ l₃` both satisfy the condition `Chain' R`, which means that the relation `R` holds between all adjacent elements in these lists, then the concatenated list `l₁ ++ l₂ ++ l₃` also satisfies the condition `Chain' R`, provided that the list `l₂` is not empty.
More concisely: If types `α` and `R` are given, and lists `l₁`, `l₂`, and `l₃` of elements of type `α` satisfy `Chain' R` for both `l₁ ++ l₂` and `l₂ ++ l₃`, then `Chain' R` holds for `l₁ ++ l₂ ++ l₃`, given that `l₂` is non-empty.
|
Mathlib.Data.List.Chain._auxLemma.3
theorem Mathlib.Data.List.Chain._auxLemma.3 : ∀ (p : Prop), (p ∧ True) = p
This theorem, `Mathlib.Data.List.Chain._auxLemma.3`, states that for any proposition `p`, the logical conjunction of `p` and the boolean `True` is equivalent to `p` itself. Symbolically, this is expressed as `p ∧ True = p`. This is a basic property of logical conjunction with the `True` statement in propositional logic.
More concisely: The theorem `Mathlib.Data.List.Chain._auxLemma.3` in Lean 4 states that `p ∧ True = p` for any proposition `p`. In other words, the conjunction of a proposition with `True` is logically equivalent to the proposition itself.
|
List.chain'_append
theorem List.chain'_append :
∀ {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α},
List.Chain' R (l₁ ++ l₂) ↔ List.Chain' R l₁ ∧ List.Chain' R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y
This theorem, `List.chain'_append`, states that for all types `α` and for all relations `R` of type `α → α → Prop`, and given two lists `l₁` and `l₂` of type `α`, the relation `R` forms a chain across the concatenation of `l₁` and `l₂` if and only if `R` forms a chain across `l₁`, forms a chain across `l₂`, and for all elements `x` in the last position of `l₁` and all elements `y` in the first position of `l₂`, `R x y` holds true. In other words, a relation forms a chain over the concatenation of two lists if it forms a chain over each list separately and also links the last element of the first list to the first element of the second list.
More concisely: For all types `α` and relations `R` on `α`, `R` is a chain over the concatenation of lists `l₁` and `l₂` if and only if `R` is a chain on `l₁`, `R` is a chain on `l₂`, and `R` relates the last element of `l₁` to the first element of `l₂`.
|
List.Chain.induction_head
theorem List.Chain.induction_head :
∀ {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α),
List.Chain r a l → (a :: l).getLast ⋯ = b → (∀ ⦃x y : α⦄, r x y → p y → p x) → p b → p a
This theorem states that given a chain of elements from `a` to `b`, a predicate `p` true for `b`, and a property that if `p` is true for `y` and `r` relates `x` and `y`, then `p` is also true for `x`, then `p` is true for `a`. In other words, the truth of this predicate can be propagated backwards along the chain from `b` to `a` if for every two adjacent elements in the chain, the property `r` allows this propagation.
More concisely: If `p(b)` holds and for all `x y` such that there exists `r` with `r` relating `x` and `y` implies `p(x)`, then `p(a)` holds for all `a` in the chain from `a` to `b`.
|
List.exists_chain_of_relationReflTransGen
theorem List.exists_chain_of_relationReflTransGen :
∀ {α : Type u} {r : α → α → Prop} {a b : α},
Relation.ReflTransGen r a b → ∃ l, List.Chain r a l ∧ (a :: l).getLast ⋯ = b
This theorem states that for any given type `α` and a binary relation `r` on `α`, if elements `a` and `b` of type `α` are related by the reflexive transitive closure of `r`, then there exists a list `l` such that `l` forms an `r`-chain starting from `a` and ending at `b`. In other words, it means that if `a` and `b` are related by a possibly reflexive (meaning that any element can relate to itself) and transitive (meaning that if an element is related to a second one, and the second one is related to a third one, the first one is related to the third one) relation, then there is a sequence of steps from `a` to `b`, each step being a relation under `r`. The converse of this theorem is `relationReflTransGen_of_exists_chain`.
More concisely: For any type `α` and binary relation `r` on `α`, if `a` and `b` are related by the reflexive transitive closure of `r`, then there exists a finite sequence of elements `[a = x₀, x₁, ..., xₙ = b]` such that `(xi, x_(i+1)) ∈ r` for all `0 ≤ i < n`.
|
List.Chain.induction
theorem List.Chain.induction :
∀ {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α),
List.Chain r a l → (a :: l).getLast ⋯ = b → (∀ ⦃x y : α⦄, r x y → p y → p x) → p b → ∀ i ∈ a :: l, p i
This theorem states that given a list representing a chain of relations from `a` to `b` and a predicate true at `b`, if the property that when relation `r` exists between `x` and `y` and the predicate is true at `y` then it's also true at `x`, then we can deduce that the predicate is true at every element in the chain, including at `a`. Basically, we can propagate the truth of the predicate up the chain.
More concisely: If for all `x y` in a list such that there exists a relation `r` between `x` and `y` implies predicate(y), then predicate(a) holds for the first element `a` of the list.
|
List.Chain'.imp
theorem List.Chain'.imp :
∀ {α : Type u} {R S : α → α → Prop},
(∀ (a b : α), R a b → S a b) → ∀ {l : List α}, List.Chain' R l → List.Chain' S l
The theorem `List.Chain'.imp` states that for any type `α` and any two relations `R` and `S` on `α`, if every pair `(a, b)` of `α` that satisfies `R` also satisfies `S`, then for any list of `α`, if `R` holds between every pair of adjacent elements in the list, then `S` also holds between every pair of adjacent elements in the list. In other words, if `S` is implied by `R` and `R` forms a chain in the list, then `S` also forms a chain in the same list.
More concisely: If relation `S` is implied by relation `R` and `R` forms a chain in a list, then `S` also forms a chain in the same list.
|
List.chain'_cons
theorem List.chain'_cons :
∀ {α : Type u} {R : α → α → Prop} {x y : α} {l : List α},
List.Chain' R (x :: y :: l) ↔ R x y ∧ List.Chain' R (y :: l)
The theorem `List.chain'_cons` states that for any type `α`, any binary relation `R` on `α`, and any elements `x` and `y` of `α` and a list `l` of elements of `α`, the relation `R` forms a chain on the list consisting of `x`, `y`, and `l` (`x :: y :: l`) if and only if `R` holds between `x` and `y` and `R` forms a chain on the list consisting of `y` and `l` (`y :: l`). In simpler terms, a list has the chain property if each consecutive pair of elements in the list satisfies the relation `R`.
More concisely: For any type `α` and binary relation `R` on `α`, the list `x :: y :: l` has the chain property with respect to `R` if and only if `R` holds between `x` and `y` and the list `y :: l` has the chain property with respect to `R`.
|
Mathlib.Data.List.Chain._auxLemma.1
theorem Mathlib.Data.List.Chain._auxLemma.1 :
∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.Chain R a (b :: l) = (R a b ∧ List.Chain R b l)
This theorem states that, for any type `α` and a relation `R` on `α`, and for any elements `a` and `b` of type `α` and list `l` of type `α`, the property that `a` is related to every element of the list `b :: l` (i.e., `b` followed by `l`) by the relation `R` (expressed as `List.Chain R a (b :: l)`) is equivalent to the conjunction of the following two conditions: `a` is related to `b` by `R` and `b` is related to every element of `l` by `R` (expressed as `R a b` and `List.Chain R b l`).
More concisely: For any type `α` and relation `R` on `α`, the element `a` is related to every element of the list `b :: l` by `R` if and only if `a` is related to `b` by `R` and `b` is related to every element of `l` by `R`. In other words, `List.Chain R a (b :: l)` is equivalent to `R a b ∧ List.Chain R b l`.
|
List.chain_map
theorem List.chain_map :
∀ {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {b : β} {l : List β},
List.Chain R (f b) (List.map f l) ↔ List.Chain (fun a b => R (f a) (f b)) b l
The `List.chain_map` theorem states that for any types `α` and `β`, a binary relation `R` on elements of type `α`, a function `f` from `β` to `α`, and a list `l` of elements of type `β` with an element `b` of type `β`, there is an equivalence between the chain relation `R` applied to the function `f` at `b` and the mapping of `f` over the list `l`, and the chain relation applied to the function `f` in a way such that `R` takes `f a` and `f b` where `a` and `b` are elements from the list `l`. This means that applying a function to each element in the list and then forming a chain relation is the same as forming a chain relation where each pair of elements is first mapped through the function.
More concisely: For any types `α` and `β`, relation `R` on `α`, function `f : β -> α`, and list `l : List β`, the chain relation `R` applied to `f` on elements from `l` is equivalent to applying `f` to each element in `l` and then applying `R` to the resulting pairs.
|
Mathlib.Data.List.Chain._auxLemma.11
theorem Mathlib.Data.List.Chain._auxLemma.11 : ∀ {α : Type u} {R : α → α → Prop} (a : α), List.Chain' R [a] = True := by
sorry
The theorem `Mathlib.Data.List.Chain._auxLemma.11` states that for any type `α`, any binary relation `R` on `α`, and any element `a` of type `α`, the property `List.Chain' R [a]` always holds true. In other words, a list composed of a single element always satisfies the chain condition for any relation `R`, as there are no adjacent elements to test the relation on.
More concisely: For any type `α` and binary relation `R` on `α`, the singleton list `[a]` satisfies the chain condition `List.Chain' R` for all `a` in `α`.
|
List.chain'_iff_pairwise
theorem List.chain'_iff_pairwise :
∀ {α : Type u} {R : α → α → Prop} [inst : IsTrans α R] {l : List α}, List.Chain' R l ↔ List.Pairwise R l
This theorem states that for any type `α`, a binary relation `R` on `α`, and a list `l` of elements of type `α`, the property that `R` holds between adjacent elements of `l` (denoted by `List.Chain' R l`) is equivalent to the property that `R` holds for every pair of elements in `l` in their order of appearance (denoted by `List.Pairwise R l`), given that `R` is transitive. In other words, if the relation `R` is transitive, then a chain of `R` in the list `l` exists if and only if `R` holds pairwise in `l`.
More concisely: If `R` is a transitive relation on type `α`, then `List.Chain' R l` holds if and only if `List.Pairwise R l` holds for any list `l` of elements of type `α`.
|
List.Chain'.cons'
theorem List.Chain'.cons' :
∀ {α : Type u} {R : α → α → Prop} {x : α} {l : List α},
List.Chain' R l → (∀ y ∈ l.head?, R x y) → List.Chain' R (x :: l)
The theorem `List.Chain'.cons'` states that for any type `α`, any binary relation `R` on `α`, any element `x` of type `α`, and any list `l` of elements of type `α`, if `R` holds between the adjacent elements of `l` (that is, `l` is a chain with respect to `R`) and `R` holds between `x` and the first element of `l` (if such an element exists), then the list obtained by prepending `x` to `l` is also a chain with respect to `R`. In other words, we can extend a chain by adding an element to the beginning, provided the new element is related to the first element of the original chain by `R`.
More concisely: If `R` is a binary relation on `α`, `l` is a chain of `α` with respect to `R`, and `x ∈ α` is related to the first element of `l` (if it exists) by `R`, then `x :: l` is also a chain of `α` with respect to `R`.
|
List.chain'_nil
theorem List.chain'_nil : ∀ {α : Type u} {R : α → α → Prop}, List.Chain' R []
The theorem `List.chain'_nil` states that for any type `α` and any binary relation `R` over `α`, the property `List.Chain' R` holds for an empty list. In other words, an empty list is considered to satisfy the "chain" condition for any given relation, since there are no pairs of elements to contradict the condition.
More concisely: For any type α and binary relation R over α, the empty list satisfies the chain condition R. (In Lean, this is expressed as `List.Chain' R []`)
|
WellFounded.list_chain'
theorem WellFounded.list_chain' :
∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → WellFounded (List.lex_chains r)
The theorem states that if a relation `r` on a type `α` is well-founded, then the lexicographic order on chains that decrease according to `r` is also well-founded. Here, a chain is a list of elements of type `α`, and a chain decreases according to `r` if each element of the chain is related to its successor by `r`. A relation is well-founded if there are no infinite sequences that decrease according to that relation. The lexicographic order on chains is a relation that compares chains by comparing their elements in sequence, from the first element onwards.
More concisely: If `r` is a well-founded relation on type `α`, then the lexicographic order on chains of `α` that decrease according to `r` is also well-founded.
|
List.relationReflTransGen_of_exists_chain
theorem List.relationReflTransGen_of_exists_chain :
∀ {α : Type u} {r : α → α → Prop} {a b : α} (l : List α),
List.Chain r a l → (a :: l).getLast ⋯ = b → Relation.ReflTransGen r a b
This theorem states that for any type `α` and any relation `r` between elements of type `α`, if there is a chain of `r` relations starting from an element `a` and ending at an element `b` in a list `l`, then `a` and `b` are related by the reflexive transitive closure of `r`. The reflexive transitive closure of a relation is the smallest relation that includes the original and is both reflexive and transitive. This theorem is the converse of `exists_chain_of_relationReflTransGen`.
More concisely: If for any type `α` and relation `r` on `α`, and elements `a` and `b` in a list `l` such that there exists a chain of `r` relations from `a` to `b`, then `a` and `b` are related by the reflexive transitive closure of `r`.
|
List.chain'_iff_get
theorem List.chain'_iff_get :
∀ {α : Type u} {R : α → α → Prop} {l : List α},
List.Chain' R l ↔ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)
The theorem `List.chain'_iff_get` states that for any given type `α`, a binary relation `R` on `α`, and list `l` of type `α`, the relation `R` forms a chain on `l` if and only if the relation `R` holds between any element at index `i` and its successor at index `i + 1` for all `i` such that `i` is less than the length of the list minus one. Here, `List.get l { val := i, isLt := ⋯ }` retrieves the element at index `i` in the list `l` and `List.Chain' R l` denotes that `R` holds between adjacent elements in `l`.
More concisely: For any type `α` and list `l` of length `n` over `α`, the relation `R` is a chain on `l` if and only if `R(l(i), l(i+1))` holds for all `0 ≤ i < n-1`.
|
List.chain_iff_pairwise
theorem List.chain_iff_pairwise :
∀ {α : Type u} {R : α → α → Prop} [inst : IsTrans α R] {a : α} {l : List α},
List.Chain R a l ↔ List.Pairwise R (a :: l)
This theorem states that for all types `α`, relation `R` that is transitive, an element `a` of type `α`, and a list `l` of elements of type `α`, the condition of the list `l` being chained from the element `a` under the relation `R` is equivalent to the list `l` with `a` prepended being pairwise related under the relation `R`. This means that if each pair of consecutive elements in the list (starting from `a`) satisfies the relation `R`, then every pair of elements in the entire list (including `a` at the start) also satisfies the relation `R`, and vice versa.
More concisely: For all types `α` and transitive relations `R` on `α`, given `a` in `α` and a list `l` of elements of `α` with `a` as prefix, `l` is chained under `R` if and only if every pair of consecutive elements in `l` is related by `R`.
|
List.chain'_cons'
theorem List.chain'_cons' :
∀ {α : Type u} {R : α → α → Prop} {x : α} {l : List α},
List.Chain' R (x :: l) ↔ (∀ y ∈ l.head?, R x y) ∧ List.Chain' R l
The theorem `List.chain'_cons'` states that for any type `α`, any binary relation `R` on `α`, any element `x` of type `α`, and any list `l` of elements of type `α`, the property that `R` holds between adjacent elements of the list `[x] concatenated with `l` (represented as `x :: l` in Lean 4) is equivalent to the conjunction of two conditions: 1) `R` holds between `x` and the first element of `l` (if `l` is not empty), and 2) `R` holds between all adjacent elements of `l`. In other words, a list starting with `x` is a chain under `R` if and only if `x` is related to the first element of the list (if it exists) under `R`, and the rest of the list is a chain under `R`.
More concisely: For any type `α` and binary relation `R` on `α`, a list `[x] :: l` of elements of `α` is a chain under `R` if and only if `R` holds between `x` and the first element of `l` (if `l` is non-empty), and `R` holds between all adjacent elements of `l`.
|
List.Chain'.tail
theorem List.Chain'.tail : ∀ {α : Type u} {R : α → α → Prop} {l : List α}, List.Chain' R l → List.Chain' R l.tail := by
sorry
This theorem states that, for any type `α` and any binary relation `R` on `α`, if a list `l` of type `α` satisfies the property `List.Chain' R`, meaning that the relation `R` holds between every pair of adjacent elements in `l`, then the tail of the list `l` (which is `l` without its first element) also satisfies the property `List.Chain' R`. In other words, if `R` holds between each pair of consecutive elements in a list, it also holds between each pair of consecutive elements in the tail of that list.
More concisely: If `R` is a binary relation on type `α` and `l` is a list of `α` with property `List.Chain' R`, then the tail of `l` also satisfies property `List.Chain' R`.
|
Mathlib.Data.List.Chain._auxLemma.2
theorem Mathlib.Data.List.Chain._auxLemma.2 : ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a [] = True
This theorem states that for any type `α`, any binary relation `R` on `α`, and any element `a` of type `α`, the property of `a` being related by `R` to every element in an empty list (denoted by `List.Chain R a []`) is always true. Essentially, it's saying that an empty list trivially satisfies the chaining condition with respect to any element and relation.
More concisely: For any type `α` and binary relation `R` on `α`, the element `a` of type `α` is related by `R` to every element in the empty list `[]`. That is, `R a []` holds.
|
Acc.list_chain'
theorem Acc.list_chain' :
∀ {α : Type u_1} {r : α → α → Prop} {l : List.chains r}, (∀ a ∈ (↑l).head?, Acc r a) → Acc (List.lex_chains r) l
This theorem states that for any type `α` and any binary relation `r` on `α`, if we have an `r`-decreasing chain `l`, and for all elements `a` that might be at the head of this chain, `a` is accessible by `r`, then the chain `l` is accessible by the lexicographic order `List.Lex r`. Here, a chain is accessible if every element in the chain can be reached from some starting point using the relation. In this context, the lexicographic order is a way to order chains, with one chain coming before another if the first differing element in the two chains is smaller in the first chain.
More concisely: Given a type `α` and a binary relation `r` on `α`, if `l` is an `r`-decreasing chain with every potential head element accessible via `r`, then `l` is accessible via the lexicographic order `List.Lex r`.
|
List.chain'_singleton
theorem List.chain'_singleton : ∀ {α : Type u} {R : α → α → Prop} (a : α), List.Chain' R [a]
The theorem `List.chain'_singleton` states that for any type `α` and any binary relation `R` on `α`, the property that `R` holds between adjacent elements in a list is true for a singleton list (a list consisting of single element `a`). In other words, every singleton list satisfies the `Chain'` condition for any given relation, since there are no pairs of adjacent elements to compare.
More concisely: For any type `α` and binary relation `R` on `α`, the singleton list `[a]` satisfies the `Chain'` condition `R` for all adjacent elements, since `R` holds vacuously.
|