Prefixes and intervals in the lexicographic order on lists

A prefix of a list is lexicographically at most that list (List.isPrefix_le), and the extensions of any prefix form an order-convex interval under the lexicographic order (List.IsPrefix.of_le_of_le, List.IsPrefix.of_prefix_of_le_of_le).

Main results

• List.isPrefix_le: if a <+: b, then a ≤ b lexicographically.
• List.IsPrefix.of_le_of_le: if p <+: b and p ≤ c ≤ b, then p <+: c.
• List.IsPrefix.of_prefix_of_le_of_le: if p <+: a, p <+: b, and a ≤ c ≤ b, then p <+: c.

theorem List.isPrefix_le {α : Type u} [LinearOrder α] {a b : List α} (h : a <+: b) : a ≤ b

A list is lexicographically at most every list it is a prefix of.

theorem List.IsPrefix.of_le_of_le {α : Type u} [LinearOrder α] {p b c : List α} (hb : p <+: b) (hpc : p ≤ c) (hcb : c ≤ b) : p <+: c

A list lexicographically between a prefix p of b and b itself also has p as a prefix.

theorem List.IsPrefix.of_prefix_of_le_of_le {α : Type u} [LinearOrder α] {p a b c : List α} (ha : p <+: a) (hb : p <+: b) (hac : a ≤ c) (hcb : c ≤ b) : p <+: c

Lists with a common prefix form a lexicographic interval.