prod_lex_of_wellFoundedOn_fiber — Mathlib

English

If the base rα is well-founded on f and each fibre over a is well-founded for rβ on g, then the lexicographic product is well-founded.

Русский

Если основание rα хорошо основано по f и каждое волокно над a хорошо основано для rβ на g, тогда лексикографическое произведение хорошо упорядочено.

LaTeX

$$WellFounded (Prod.Lex rα rβ on fun c => (f c, g c))$$

Lean4

theorem prod_lex_of_wellFoundedOn_fiber (hα : s.WellFoundedOn (rα on f))
    (hβ : ∀ a, (s ∩ f ⁻¹' { a }).WellFoundedOn (rβ on g)) : s.WellFoundedOn (Prod.Lex rα rβ on fun c => (f c, g c)) :=
  WellFounded.prod_lex_of_wellFoundedOn_fiber hα fun a ↦
    ((hβ a).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun _ _ h ↦ ‹_›)

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