wellFounded' — Mathlib

English

Under a trichotomy assumption on the index relation and a well-founded swap of the base order, the Lex order is well-founded.

Русский

При трёхчётности порядка индексов и хорошо основанного обратного порядка, Lex хорошо основан.

LaTeX

$$$\\mathrm{WellFounded'}(DFinsupp.Lex(r,s))$ under IsTrichotomous and swap-well-founded hr$$

Lean4

theorem wellFounded' (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFounded (s i)) [IsTrichotomous ι r]
    (hr : WellFounded (Function.swap r)) : WellFounded (DFinsupp.Lex r s) :=
  Lex.wellFounded hbot hs <|
    Subrelation.wf (fun {i j} h => ((@IsTrichotomous.trichotomous ι r _ i j).resolve_left h.1).resolve_left h.2) hr

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