wellFounded — Mathlib

English

If the base relation is well-founded and the coordinates are well-founded, then the Lex order on DFinsupp is well-founded.

Русский

Если базовое отношение хорошо основано и координаты тоже, то порядок Lex над DFinsupp хорошо основан.

LaTeX

$$$\\mathrm{WellFounded}(DFinsupp.Lex(r,s))\\;\\text{given } hbot,\\; hs,\\; hr$$$

Lean4

theorem wellFounded (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFounded (s i)) (hr : WellFounded <| rᶜ ⊓ (· ≠ ·)) :
    WellFounded (DFinsupp.Lex r s) :=
  ⟨fun x => by classical exact Lex.acc hbot hs x fun i _ => hr.apply i⟩

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