PSigma.lex_wf

theorem PSigma.lex_wf : ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop}, WellFounded r → (∀ (x : α), WellFounded (s x)) → WellFounded (PSigma.Lex r s)

This theorem is concerned with the well-foundedness of relations in the context of dependent types or sorts. It states that for any two sorts `α` and `β`, where `β` is dependent on `α`, and two relations `r` and `s`, where `r` is a relation on `α` and `s` is a dependent relation on `β`, if `r` and `s x` (for any `x` in `α`) are well-founded, then the lexicographical order, denoted by `PSigma.Lex r s`, of these relations is also well-founded.

More concisely: If `r` is a well-founded relation on sort `α`, and `s(x)` is a well-founded dependent relation on sort `β` for all `x` in `α`, then the lexicographical order `PSigma.Lex r s` of `r` and `s` is a well-founded relation.