English
The lexicographic order on PSigma is well-founded given well-foundedness of the base relation.
Русский
Лексикографический порядок на PSigma хорошо основан при установленности базового отношения.
LaTeX
$$$[\\text{WellFounded } r] \\Rightarrow [\\forall x, \\text{WellFounded } (s x)] \\Rightarrow \\text{WellFounded } (PSigma.Lex r s)$$$
Lean4
/-- The lexicographical order of well-founded relations is well-founded. -/
theorem psigma_lex {α : Sort*} {β : α → Sort*} {r : α → α → Prop} {s : ∀ a : α, β a → β a → Prop} (ha : WellFounded r)
(hb : ∀ x, WellFounded (s x)) : WellFounded (Lex r s) :=
WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) hb b
