English
Let α be a type and r a relation on α with decidable comparison. If l and c are lists with c a sublist of l, and for every a' in c we have a ≼ a' (with respect to r), then the list a :: c is a sublist of the list obtained by inserting a into l in a way that preserves the order given by r; i.e. a :: c <+ orderedInsert r a l.
Русский
Пусть α — тип, r — отношение на α с разрешенным сравнением. Пусть l и c — списки, где c является подпоследовательностью (подсписком) l, и для каждого a' ∈ c выполняется a ≼ a' относительно r. Тогда список a :: c является подпоследовательностью к списку, получаемому вставкой a в l в порядке, заданном r; a :: c <+ orderedInsert r a l.
LaTeX
$$$ c <+ l \\ \\wedge\\ (\\forall a' \\in c,\\ a \\preceq a') \\Rightarrow a :: c <+ orderedInsert r a l $$$
Lean4
theorem cons_sublist_orderedInsert {l c : List α} {a : α} (hl : c <+ l) (ha : ∀ a' ∈ c, a ≼ a') :
a :: c <+ orderedInsert r a l := by
induction l with
| nil => simp_all only [sublist_nil, orderedInsert, Sublist.refl]
| cons _ _ ih =>
unfold orderedInsert
split_ifs with hr
· exact .cons₂ _ hl
·
cases hl with
| cons _ h => exact .cons _ <| ih h
| cons₂ => exact absurd (ha _ <| mem_cons_self ..) hr
