sigma_lex_of_wellFoundedOn_fiber — Mathlib

English

A fiberwise construction shows that σ-lex well-foundedness propagates along a base-well-founded structure.

Русский

Построение по волокнам сохраняет хорошо основанность для σ-лекс по базовому основанию.

LaTeX

$$Set.WellFoundedOn sigma_lex_of_wellFoundedOn_fiber$$

Lean4

theorem sigma_lex_of_wellFoundedOn_fiber (hι : s.WellFoundedOn (rι on f))
    (hπ : ∀ i, (s ∩ f ⁻¹' { i }).WellFoundedOn (rπ i on g i)) :
    s.WellFoundedOn (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩) :=
  by
  change WellFounded (Sigma.Lex rι rπ on fun c : s => ⟨f c, g (f c) c⟩)
  exact
    @WellFounded.sigma_lex_of_wellFoundedOn_fiber _ s _ _ rπ (fun c => f c) (fun i c => g _ c) hι fun i =>
      ((hπ i).onFun (f := fun x => ⟨x, x.1.2, x.2⟩)).mono (fun b c h => ‹_›)

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