Pair sublists as positional order #
List.pair_sublist_iff_idxOf_lt: on a Nodup list, [a, b] <+ l says exactly that
a and b are members with a at a strictly earlier index — the pair-sublist
relation is the strict linear order a duplicate-free list carries.
theorem
List.pair_sublist_of_idxOf_lt
{α : Type u_1}
[DecidableEq α]
{a b : α}
{l : List α}
(ha : a ∈ l)
(hb : b ∈ l)
(h : idxOf a l < idxOf b l)
:
[a, b].Sublist l
theorem
List.idxOf_lt_of_pair_sublist
{α : Type u_1}
[DecidableEq α]
{a b : α}
{l : List α}
(hnd : l.Nodup)
(h : [a, b].Sublist l)
:
theorem
List.pair_sublist_iff_idxOf_lt
{α : Type u_1}
[DecidableEq α]
{a b : α}
{l : List α}
(hnd : l.Nodup)
:
[a, b].Sublist l ↔ a ∈ l ∧ b ∈ l ∧ idxOf a l < idxOf b l
On a Nodup list, the pair-sublist relation is the strict positional order.