wellFounded_isDershowitzMannaLT — Mathlib

English

Over a well-founded order, the Dershowitz–Manna order on multisets is well-founded when α is well-founded.

Русский

Для хорошо основанного порядка на α порядок Дершовиц-Манна на мультисетах хорошо основан.

LaTeX

$$$[WellFoundedLT\\,\\alpha] \\Rightarrow WellFounded (IsDershowitzMannaLT:\\mathcal{M}(\\alpha)\\to\\mathcal{M}(\\alpha)\\to \\mathrm{Prop}).$$$

Lean4

/-- Over a well-founded order, the Dershowitz-Manna order on multisets is well-founded. -/
theorem wellFounded_isDershowitzMannaLT [WellFoundedLT α] :
    WellFounded (IsDershowitzMannaLT : Multiset α → Multiset α → Prop) :=
  by
  rw [← transGen_oneStep_eq_isDershowitzMannaLT]
  exact isDershowitzMannaLT_singleton_wf.transGen

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