sort_cons — Mathlib

English

If every b in s satisfies r(a,b), then sort r(cons a s) = cons a (sort r s).

Русский

Если для каждого b ∈ s выполняется r(a,b), то sort r (cons a s) = cons a (sort r s).

LaTeX

$$$$ (\\forall b \\in s,\\ r\\ a\\ b) \\Rightarrow \\operatorname{sort} r (\\operatorname{cons} a s) = \\operatorname{cons} a (\\operatorname{sort} r s) $$$$

Lean4

theorem sort_cons (a : α) (s : Multiset α) : (∀ b ∈ s, r a b) → sort r (a ::ₘ s) = a :: sort r s :=
  by
  refine Quot.inductionOn s fun l => ?_
  simpa [mergeSort_eq_insertionSort] using insertionSort_cons r (a := a) (l := l)

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