List.forall₂_same
theorem List.forall₂_same : ∀ {α : Type u_1} {Rₐ : α → α → Prop} {l : List α}, List.Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x
This theorem states that for any type `α` and any binary relation `Rₐ` on elements of `α`, and any list `l` of elements of type `α`, `List.Forall₂ Rₐ l l` if and only if for every element `x` in the list `l`, `Rₐ x x` holds. In other words, every element in the list satisfies the relation with itself if and only if the relation holds pairwise between corresponding elements of the list and itself.
More concisely: For any type `α` and binary relation `R` on `α`, `List.Forall₂ R l l` if and only if for all `x` in `l`, `R x x`.
|
List.sublistForall₂_iff
theorem List.sublistForall₂_iff :
∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
List.SublistForall₂ R l₁ l₂ ↔ ∃ l, List.Forall₂ R l₁ l ∧ l.Sublist l₂
This theorem states that for any two given types `α` and `β`, a relation `R` between `α` and `β`, and two lists `l₁` of type `α` and `l₂` of type `β`, `l₁` is a sublist of `l₂` with all pairs of elements satisfying the relation `R` if and only if there exists a list `l` such that `l₁` and `l` satisfy the relation `R` for all pairs of their elements and `l` is a sublist of `l₂`.
More concisely: For types `α` and `β`, relation `R` between them, and lists `l₁` of type `α` and `l₂` of type `β`, `l₁` is a sublist of `l₂` preserving `R` if and only if there exists a sublist `l` of `l₂` such that `l₁` and `l` have `R`-related elements.
|
List.forall₂_refl
theorem List.forall₂_refl :
∀ {α : Type u_1} {Rₐ : α → α → Prop} [inst : IsRefl α Rₐ] (l : List α), List.Forall₂ Rₐ l l
This theorem states that for any type `α` and a binary predicate `Rₐ` on `α`, given that `Rₐ` is reflexive (as specified by `IsRefl α Rₐ`), for any list `l` of type `List α`, `List.Forall₂ Rₐ l l` holds true. In other words, each element in the list `l` is in relation `Rₐ` with itself.
More concisely: For any type `α` and reflexive binary relation `Rₐ` on `α`, `List.Forall₂ Rₐ l l` holds for all lists `l` of type `List α`. That is, each element in `l` is related to itself via `Rₐ`.
|