A chain of intervals that is pairwise apart #
A candidate for Mathlib.Data.List.Chain: a chain of intervals [l, u] with l ≤ u, each ending
below the start of the next, is pairwise so.
Main statements #
List.pairwise_of_isChain_of_le: a chain of intervals, each ending below the start of the next, is pairwise so.
theorem
List.pairwise_of_isChain_of_le
{α : Type u_1}
[Preorder α]
{l : List (α × α)}
(h1 : ∀ (i : α × α), i ∈ l → i.fst ≤ i.snd)
(h2 : IsChain (fun (i j : α × α) => i.snd < j.fst) l)
:
A chain of intervals [l, u] with l ≤ u, each ending below the start of the next, is pairwise
so: the relation is transitive on such intervals.