The entries of a sorted list below a bound come first #
A candidate for Mathlib.Data.List.Sort: in a sorted list (List.SortedLE), the entries below a
bound t are its first entries, so entry i is below t when i is below their number.
Main statements #
List.SortedLE.getElem_lt_of_lt_length_filter: entryiof a sorted list is belowtwheniis below the number of entries belowt.
theorem
List.SortedLE.getElem_lt_of_lt_length_filter
{α : Type u_1}
[Preorder α]
[DecidableLT α]
{l : List α}
(hl : l.SortedLE)
{t : α}
{i : ℕ}
(hi : i < (filter (fun (x : α) => decide (x < t)) l).length)
:
In a sorted list, the entries below t come first: entry i is below t when i is below
the number of entries below t, since an entry not below t has no entry below t after it.