English
Proof that a finite product of well-ordered sets is PWOn, via a finite induction on the index set.
Русский
Доказательство того, что конечный прямой произведение хорошо упорядочено, через конечную индукцию над индексным множеством.
LaTeX
$$theorem isPWO {α : ι → Type*} [∀ i, LinearOrder (α i)] [∀ i, IsWellOrder (α i) (· < ·)] [Finite ι] (s : Set (∀ i, α i)) : s.IsPWO$$
Lean4
/-- Stronger version of `WellFounded.prod_lex`. Instead of requiring `rβ on g` to be well-founded,
we only require it to be well-founded on fibers of `f`. -/
theorem prod_lex_of_wellFoundedOn_fiber (hα : WellFounded (rα on f)) (hβ : ∀ a, (f ⁻¹' { a }).WellFoundedOn (rβ on g)) :
WellFounded (Prod.Lex rα rβ on fun c => (f c, g c)) :=
by
refine
((psigma_lex (wellFoundedOn_range.2 hα) fun a => hβ a).onFun (f := fun c => ⟨⟨_, c, rfl⟩, c, rfl⟩)).mono
fun c c' h => ?_
obtain h' | h' := Prod.lex_iff.1 h
· exact PSigma.Lex.left _ _ h'
· dsimp only [InvImage, (· on ·)] at h' ⊢
convert PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1; swap
exacts [⟨c, h'.1⟩, PSigma.subtype_ext (Subtype.ext h'.1) rfl, h'.2]
