instWellFoundedLT — Mathlib

English

The Less-Than relation on multisets is well-founded provided α is endowed with a well-founded LT.

Русский

Относение меньше чем на мультисетах является хорошо основанным, если на α задан порядок LT, который хорошо основан.

LaTeX

$$$\\text{WellFoundedLT}(\\mathcal{M}(\\alpha))$$$

Lean4

/-- Another way of expressing `strongInductionOn`: the `(<)` relation is well-founded. -/
instance instWellFoundedLT : WellFoundedLT (Multiset α) :=
  ⟨Subrelation.wf Multiset.card_lt_card (measure Multiset.card).2⟩

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