List.pairwise_pwFilter
theorem List.pairwise_pwFilter :
∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] (l : List α), List.Pairwise R (List.pwFilter R l) := by
sorry
The theorem `List.pairwise_pwFilter` states that for any type `α`, any binary relation `R` on `α` that is decidable, and any list `l` of elements of type `α`, the list obtained by applying the `pwFilter` operation with the relation `R` to the list `l` is a pairwise `R`-related list. In other words, for every pair of distinct elements in the filtered list, the relation `R` holds between those elements.
More concisely: Let `α` be a type, `R` be a decidable binary relation on `α`, and `l` be a list of `α`. The `pwFilter l R` is a sublist of `l` such that for all distinct `x` and `y` in `pwFilter l R`, `x R y` holds.
|
List.pairwise_singleton
theorem List.pairwise_singleton : ∀ {α : Type u_1} (R : α → α → Prop) (a : α), List.Pairwise R [a]
This theorem states that for any type `α` and any binary relation `R` over `α`, a singleton list containing an element `a` of type `α` is pairwise related by `R`. In other words, `List.Pairwise R [a]` always holds true since there are no distinct pair of elements in the list to contradict the pairwise property.
More concisely: For any type `α` and binary relation `R` over `α`, the singleton list `[a]` (where `a : α`) satisfies the pairwise property `R` (i.e., `List.Pairwise R [a]` holds true).
|
List.pairwise_iff_get
theorem List.pairwise_iff_get :
∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
This theorem states that for any type `α`, any binary relation `R` on `α`, and any list `l` of elements of type `α`, the list `l` is pairwise related by `R` if and only if, for any pair of natural numbers `i` and `j` such that `i` is less than `j` and both are valid indices into the list `l` (i.e., they are less than the length of `l`), the `i`-th element of `l` is related to the `j`-th element of `l` by `R`. In other words, a list is pairwise related by a relation if every pair of elements in the list that occur in a specific order satisfy that relation.
More concisely: For any type `α` and binary relation `R` on `α`, a list `l` of elements of type `α` is pairwise related by `R` if and only if for all i < j, the i-th and j-th elements of `l` are related by `R`.
|
List.Pairwise.of_cons
theorem List.Pairwise.of_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : α → α → Prop}, List.Pairwise R (a :: l) → List.Pairwise R l
This theorem states that for any type `α`, any element `a` of type `α`, any list `l` of type `α`, and any relation `R` defined over `α`, if the list composed of `a` followed by `l` satisfies the pairwise property with respect to `R`, then the list `l` also satisfies the pairwise property with respect to `R`. The pairwise property implies that for every pair of distinct elements in the list, the relation `R` holds.
More concisely: If a list `l` of type `α` satisfies the pairwise property of relation `R` with respect to its head `a` and the tail of the list, then `l` itself satisfies the pairwise property of relation `R`.
|
List.map_get_sublist
theorem List.map_get_sublist :
∀ {α : Type u_1} {l : List α} {is : List (Fin l.length)},
List.Pairwise (fun x x_1 => ↑x < ↑x_1) is → (List.map l.get is).Sublist l
The theorem `List.map_get_sublist` states that for any type `α`, given a list `l` of elements of type `α` and a list `is` of indices into `l` (expressed as elements of the `Fin` type, which are non-negative integers less than `l.length`), if `is` is pairwise strictly increasing (i.e., every element of `is` is less than the next one), then the list obtained by mapping the `get` function over `is` (i.e., by retrieving the elements of `l` at the indices specified by `is`) is a sublist of `l`. This means that getting elements from a list at monotonically increasing indices always produces a sublist of the original list.
More concisely: For any type `α` and lists `l:` `List α` and `is:` `List (Fin (l.length))` with `is` pairwise strictly increasing, `List.map get is ⊆ l`.
|
List.pwFilter_cons_of_neg
theorem List.pwFilter_cons_of_neg :
∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {a : α} {l : List α},
(¬∀ b ∈ List.pwFilter R l, R a b) → List.pwFilter R (a :: l) = List.pwFilter R l
The theorem `List.pwFilter_cons_of_neg` states that for any type `α`, any decidable relation `R` on `α`, and any elements `a` of type `α` and `l` of type List `α`, if it is not the case that `R` holds for `a` and all elements in the pairwise filter of `l` with respect to `R`, then the pairwise filter of the list obtained by prepending `a` to `l` with respect to `R` is the same as the pairwise filter of `l` with respect to `R`. In other words, if `a` does not satisfy the relation `R` with every element in the pairwise filtered list `l`, then `a` is not included in the pairwise filtered list of `a :: l`.
More concisely: If `α` is a type with decidable relation `R`, and `a` is not in the pairwise filter of `l` with respect to `R`, then `a` is not in the pairwise filter of `a :: l` with respect to `R`.
|
List.pwFilter_cons_of_pos
theorem List.pwFilter_cons_of_pos :
∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {a : α} {l : List α},
(∀ b ∈ List.pwFilter R l, R a b) → List.pwFilter R (a :: l) = a :: List.pwFilter R l
The theorem `List.pwFilter_cons_of_pos` states that for any type `α`, any decidable relation `R` on `α`, any element `a` of `α`, and any list `l` of `α`, if `a` has the relation `R` with all elements in the list obtained by applying the `pwFilter` function with the relation `R` to the list `l`, then applying the `pwFilter` function with the relation `R` to the list obtained by prepending `a` to `l` results in the list obtained by prepending `a` to the list obtained by applying the `pwFilter` function with the relation `R` to `l`. In other words, if all elements in the `pwFilter` of a list satisfy a certain relation with a given element, then this element stays at the head of the list when we apply `pwFilter`.
More concisely: If `a` is in the `pwFilter` of `l` with respect to relation `R`, then `a` is at the head of the `pwFilter` of the list `a :: l`.
|
List.Pairwise.iff_of_mem
theorem List.Pairwise.iff_of_mem :
∀ {α : Type u_1} {R S : α → α → Prop} {l : List α},
(∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b)) → (List.Pairwise R l ↔ List.Pairwise S l)
This theorem states that for any list `l` of elements of some type `α`, and for any two relations `R` and `S` on the elements of `α`, if for all pairs of elements `a` and `b` in `l`, `a` is related to `b` by `R` if and only if `a` is related to `b` by `S`, then the list `l` is a pairwise `R`-list if and only if it is a pairwise `S`-list. Here, a pairwise `R`-list means that every pair of distinct elements in the list satisfies the relation `R`.
More concisely: If for all distinct elements `a` and `b` in list `l` of type `α`, `a` is related to `b` under relations `R` if and only if they are related under `S`, then `l` is a pairwise `R`-list if and only if it is a pairwise `S`-list.
|
List.sublist_eq_map_get
theorem List.sublist_eq_map_get :
∀ {α : Type u_1} {l' l : List α},
l'.Sublist l → ∃ is, l' = List.map l.get is ∧ List.Pairwise (fun x x_1 => x < x_1) is
The theorem `List.sublist_eq_map_get` states that for any sublist `l'` of a list `l` of arbitrary type `α`, there exists a list of indices `is` such that `l'` is equal to the list obtained by applying the `get` function of `l` to each element in `is`. Moreover, the elements in the list of indices `is` are pairwise strictly increasing, which means for every pair of elements `x` and `x_1` in `is`, `x` is less than `x_1`. The `get` function retrieves the element of a list at a given index.
More concisely: For any sublist $l'$ of a list $l$ and indices $i\_1, i\_2, \dots, i\_n$ in $l$ such that $i\_1 < i\_2 < \dots < i\_n$, we have $l' = \{\ get(l, i\_1), get(l, i\_2), \dots, get(l, i\_n) \}$.
|
List.Pairwise.imp_of_mem
theorem List.Pairwise.imp_of_mem :
∀ {α : Type u_1} {l : List α} {R S : α → α → Prop},
(∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → List.Pairwise R l → List.Pairwise S l
This theorem states that, for any type `α` and any list `l` of type `α`, given two properties `R` and `S` of pairs of objects of type `α`, if for every pair of elements `a` and `b` in `l`, whenever `R a b` holds then `S a b` also holds, then if all pairs of elements in `l` have property `R`, it follows that all pairs of elements in `l` also have property `S`. In more mathematical language, it's saying that if `R` implies `S` for all pairs in the list, and the list is pairwise `R`, then the list is also pairwise `S`.
More concisely: If `R` implies `S` between any pair of elements in a list `l` of type `α`, and every pair in `l` has property `R`, then `l` has the property `S` between all pairs.
|
List.pairwise_iff_forall_sublist
theorem List.pairwise_iff_forall_sublist :
∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, List.Pairwise R l ↔ ∀ {a b : α}, [a, b].Sublist l → R a b := by
sorry
This theorem states that for any type `α`, any list `l` of `α`, and any binary relationship `R` on `α`, the list `l` has the property `Pairwise R` (meaning that for every pair of elements in the list, `R` holds) if and only if for any elements `a` and `b` of type `α`, if the list `[a, b]` is a sublist of `l`, then `R a b` holds. In other words, the list `l` satisfies the pairwise property with respect to `R` precisely when `R` holds for any pair of elements that appear consecutively in `l`.
More concisely: For any type `α`, list `l` of `α`, and binary relation `R` on `α`, `l` has property `Pairwise R` if and only if for all `a` and `b` in `α`, if `[a, b]` is a sublist of `l`, then `R a b`.
|