perm_orderedInsert — Mathlib

English

For any a, l: List α, the list obtained by inserting a into l is a permutation of a :: l.

Русский

Для любого элемента a и списка l: вставка a в l порождает перестановку списка a :: l.

LaTeX

$$$$ \forall a:\alpha,\forall l:\mathrm{List}(\alpha),\; \mathrm{orderedInsert}(r,a,l) \;\sim\; \mathrm{List.cons}(a,l). $$$$

Lean4

theorem perm_orderedInsert (a) : ∀ l : List α, orderedInsert r a l ~ a :: l
  | [] => Perm.refl _
  | b :: l => by
    by_cases h : a ≼ b
    · simp [orderedInsert, h]
    · simpa [orderedInsert, h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

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