cutExpand — Mathlib

English

If the relation r is well-founded, then CutExpand r is well-founded on multisets.

Русский

Если отношение r хорошо основано, то CutExpand r хорошо основано на мультисетах.

LaTeX

$$$ WellFounded(r) \Rightarrow WellFounded(CutExpand(r)) $$$

Lean4

/-- `CutExpand r` is well-founded when `r` is. -/
theorem _root_.WellFounded.cutExpand (hr : WellFounded r) : WellFounded (CutExpand r) :=
  ⟨have := hr.isIrrefl;
    fun _ ↦ acc_of_singleton fun a _ ↦ (hr.apply a).cutExpand⟩

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