List.pairwise_cons
theorem List.pairwise_cons :
∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α},
List.Pairwise R (a :: l) ↔ (∀ a' ∈ l, R a a') ∧ List.Pairwise R l
This theorem, `List.pairwise_cons`, is about lists in Lean 4. It states that for any type `α`, any relation `R` on `α`, any element `a` of `α`, and any list `l` of elements of `α`, the list `a` followed by `l` (`a :: l`) is pairwise related by `R` if and only if (1) every element `a'` in the list `l` is related to `a` by `R` and (2) `l` is pairwise related by `R`. In more plain language, the first element of the list is related by `R` to every other element, and every pair of elements in the remainder of the list are also related by `R`.
More concisely: For any type `α` and relation `R` on `α`, the list `[a] ++ l` is pairwise related by `R` if and only if `a` is related to every element in `l` by `R` and `l` is pairwise related by `R`.
|
List.Forall₂.brecOn
theorem List.Forall₂.brecOn :
∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
{motive : (a : List α) → (a_1 : List β) → List.Forall₂ R a a_1 → Prop} {a : List α} {a_1 : List β}
(x : List.Forall₂ R a a_1),
(∀ (a : List α) (a_2 : List β) (x : List.Forall₂ R a a_2), x.below → motive a a_2 x) → motive a a_1 x
This theorem, `List.Forall₂.brecOn`, states that for any two lists of types `α` and `β` respectively, and a relation `R` between elements of `α` and `β`, if `R` holds for all corresponding pairs of elements from the two lists, then for any property or motive `motive` that depends on a pair of lists and the fact that `R` holds for all corresponding elements, if this `motive` holds for any pair of lists and their relation whenever it holds for all 'smaller' pairs (this is captured by the `List.Forall₂.below` predicate), then it holds for the original pair of lists. This is a kind of induction principle for relations over pairs of lists.
More concisely: If a relation holds between corresponding elements of two lists and it is closed under the `List.Forall₂.below` predicate, then it holds for the entire pair of lists.
|
List.Sublist.brecOn
theorem List.Sublist.brecOn :
∀ {α : Type u_1} {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} {a a_1 : List α} (x : a.Sublist a_1),
(∀ (a a_2 : List α) (x : a.Sublist a_2), x.below → motive a a_2 x) → motive a a_1 x
This is a theorem about recursively applying a motive (a predicate or property) to a pair of lists and a proof that the first list is a sublist of the second. Given a type `α`, a motive that applies to pairs of lists of `α` and a proof that one is a sublist of the other, and specific lists `a` and `a_1` with a proof `x` that `a` is a sublist of `a_1`, the theorem states that if the motive holds for any pair of lists and a sublist proof where the motive holds for all "smaller" sublists, then the motive holds for `a` and `a_1` with the sublist proof `x`. This is essentially a principle of mathematical induction for the structure of sublists.
More concisely: If a motive holds for all pairs of sublists and their sublist proofs, then it holds for a given sublist `a` of a larger list `a_1` with their corresponding sublist proof `x`.
|