wellFounded' — Mathlib

English

A variant of well-foundedness for Finsupp.Lex under trichotomy and swapped base relation.

Русский

Вариант хорошо основанности для Finsupp.Lex при тройственности и перестановке отношения.

LaTeX

$$$WellFounded (Finsupp.Lex r s)$$$

Lean4

theorem wellFounded' (hbot : ∀ ⦃n⦄, ¬s n 0) (hs : WellFounded s) [IsTrichotomous α r]
    (hr : WellFounded (Function.swap r)) : WellFounded (Finsupp.Lex r s) :=
  (lex_eq_invImage_dfinsupp_lex r s).symm ▸ InvImage.wf _ (DFinsupp.Lex.wellFounded' (fun _ => hbot) (fun _ => hs) hr)

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