List.Pairwise.forall_of_forall
theorem List.Pairwise.forall_of_forall :
∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
Symmetric R → (∀ x ∈ l, R x x) → List.Pairwise R l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
The theorem `List.Pairwise.forall_of_forall` states that for all types `α`, all binary relations `R` on `α`, and all lists `l` of type `α`, if `R` is a symmetric relation and for every element `x` in the list `l`, `x` is related to itself under `R`, and if `l` is a pairwise R-list, then for any two elements `x` and `y` in the list `l`, `x` is related to `y` under `R`.
In other words, this theorem is saying if a relation is symmetric and each element in the list is related to itself via this relation, and if every pair of distinct elements in the list are related via this relation (pairwise property), then every two elements in the list are related via this relation.
More concisely: If `R` is a symmetric relation on type `α` such that for all `x` in list `l` of type `α`, `x` is related to itself under `R` and `l` is a pairwise `R`-list, then for all `x` and `y` in `l`, `x` is related to `y` under `R`.
|
List.Pairwise.pwFilter
theorem List.Pairwise.pwFilter :
∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {l : List α},
List.Pairwise R l → List.pwFilter R l = l
The theorem `List.Pairwise.pwFilter` states that for all types `α` and relations `R` on `α`, which are decidable (meaning that for any two elements of `α`, it can be decided whether the relation holds or not), and for all lists `l` of type `α`, if the list `l` is pairwise with respect to the relation `R`, then applying the pairwise filter function `List.pwFilter` to the list `l` with the relation `R` will result in the original list `l`. In other words, if all pairs of elements in `l` satisfy the relation `R`, then the pairwise filter operation will not change `l`. This theorem is an alias for the reverse direction of theorem `List.pwFilter_eq_self`.
More concisely: If `α` is a type with a decidable relation `R`, and `l : List α` is pairwise with respect to `R`, then `List.pwFilter l R = l`.
|
List.Pairwise.pmap
theorem List.Pairwise.pmap :
∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {l : List α},
List.Pairwise R l →
∀ {p : α → Prop} {f : (a : α) → p a → β} (h : ∀ x ∈ l, p x) {S : β → β → Prop},
(∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)) → List.Pairwise S (List.pmap f l h)
This theorem states that for any two types `α` and `β`, a relation `R` on elements of type `α`, and a list of elements of type `α`, if the elements of the list are pairwise related by `R`, then for any predicate `p` on elements of type `α`, and a function `f` from elements of `α` satisfying `p` to `β`, if every element in the list satisfies `p`, and there's a relation `S` on elements of type `β` such that for any two elements `x` and `y` of `α` satisfying `p`, if `x` and `y` are related by `R` then the images of `x` and `y` under `f` are related by `S`, then the elements of the list obtained by mapping `f` over the original list are pairwise related by `S`.
More concisely: Given types `α`, `β`, a relation `R` on `α`, a list `ls : list α`, a predicate `p` on `α`, a function `f : {x : α | p x} -> β`, and a relation `S` on `β`, if every pair of related elements in `ls` satisfy `p` and the image of every pair of `p`-related elements under `f` are related by `S`, then the images of the list under `f` are pairwise related by `S`.
|