sublist_orderedInsert — Mathlib

English

For any x and xs, xs is a sublist of xs.orderedInsert r x.

Русский

Для любого x и xs, xs является подсписком xs.orderedInsert r x.

LaTeX

$$$$ \forall x:\alpha,\forall xs:\mathrm{List}(\alpha),\; xs \\subseteq\\ xs.\operatorname{orderedInsert}(r,x). $$$$

Lean4

theorem sublist_orderedInsert (x : α) (xs : List α) : xs <+ xs.orderedInsert r x :=
  by
  rw [orderedInsert_eq_take_drop]
  refine Sublist.trans ?_ (.append_left (.cons _ (.refl _)) _)
  rw [takeWhile_append_dropWhile]

Похожие утверждения