English
Another formulation of the fiber-based well-foundedness for a product lexicographic order.
Русский
Другая формулировка условного базиса для произведения лексикографического порядка.
LaTeX
$$WellFounded (Function.onFun (Prod.Lex rα rβ) fun c => { fst := f c, snd := g c })$$
Lean4
/-- Stronger version of `PSigma.lex_wf`. Instead of requiring `rπ on g` to be well-founded, we only
require it to be well-founded on fibers of `f`. -/
theorem sigma_lex_of_wellFoundedOn_fiber (hι : WellFounded (rι on f))
(hπ : ∀ i, (f ⁻¹' { i }).WellFoundedOn (rπ i on g i)) :
WellFounded (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) 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', h''⟩ := Sigma.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
· exact ⟨c, h'⟩
· exact PSigma.subtype_ext (Subtype.ext h') rfl
· dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *
grind
