instIsWellFoundedMultisetCutExpand

English

If α with relation r is well-founded, then the CutExpand relation on Multiset α is well-founded.

Русский

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

LaTeX

$$$ [IsWellFounded(\alpha, r)] \Rightarrow IsWellFounded( Multiset(\alpha), CutExpand(r) ) $$$

Lean4

instance [h : IsWellFounded α r] : IsWellFounded _ (CutExpand r) :=
  ⟨h.wf.cutExpand⟩

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