wellFoundedLT' — Mathlib

English

For any Finite set α and Preorder N with LT, the function space α →₀ N is well-founded in the LT sense.

Русский

Для любого конечного множества α и частично упорядоченного N с LT множество функций α →₀ N хорошо основано по LT.

LaTeX

$$$WellFoundedLT (Finsupp\, α\, N)$$$

Lean4

instance wellFoundedLT' {N} [AddMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] [WellFoundedLT N] :
    WellFoundedLT (α →₀ N) :=
  Finsupp.wellFoundedLT fun a => (zero_le a).not_gt

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