English
If a base step gives Acc for a single coordinate, then Acc holds for every value at that coordinate in the Lex-ordered single position.
Русский
Если базовый шаг даёт Acc для единичной координаты, то Acc держится для любого значения в Lex-единичном положении.
LaTeX
$$$\\forall i,\\ Acc(r^c\\cap(\\cdot \\neq \\cdot)) i \\Rightarrow \\forall a,\\ Acc(DFinsupp.Lex(r,s)) (single i a)$$$
Lean4
protected theorem wellFoundedLT [∀ i, Zero (α i)] [∀ i, Preorder (α i)] [∀ i, WellFoundedLT (α i)]
(hbot : ∀ ⦃i⦄ ⦃a : α i⦄, ¬a < 0) : WellFoundedLT (Π₀ i, α i) :=
⟨by
set β := fun i ↦ Antisymmetrization (α i) (· ≤ ·)
set e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization (· ≤ ·)
let _ : ∀ i, Zero (β i) := fun i ↦ ⟨e i 0⟩
have :
WellFounded (DFinsupp.Lex (Function.swap <| @WellOrderingRel ι) (fun _ ↦ (· < ·) : (i : ι) → β i → β i → Prop)) :=
by
have := IsTrichotomous.swap (@WellOrderingRel ι)
refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
· rintro i ⟨a⟩
apply hbot
· simp +unfoldPartialApp only [Function.swap]
exact IsWellFounded.wf
refine Subrelation.wf (fun h => ?_) <| InvImage.wf (mapRange e fun _ ↦ rfl) this
have := IsStrictOrder.swap (@WellOrderingRel ι)
obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder (Function.swap WellOrderingRel) h
exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩⟩
