bubble_sort_induction — Mathlib

English

Bubble sort induction (non-prioritized): if a property P holds for a sequence f and is preserved under swapping adjacent elements in permutations, then P holds for the sorted version of f.

Русский

Индукция пузырьковой сортировки: если свойство P выполняется для последовательности f и сохраняется при обмене соседних элементов в перестановках, тогда P верно и для отсортированной версии f.

LaTeX

$$$P f \\rightarrow (\\forall (g,i,j), i

Lean4

/-- *Bubble sort induction*: Prove that the sorted version of `f` has some property `P`
if `f` satisfies `P` and `P` is preserved when swapping two antitone values. -/
theorem bubble_sort_induction {n : ℕ} {α : Type*} [LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop} (hf : P f)
    (h : ∀ (g : Fin n → α) (i j : Fin n), i < j → g j < g i → P g → P (g ∘ Equiv.swap i j)) : P (f ∘ sort f) :=
  bubble_sort_induction' hf fun _ => h _

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