Sigma.lex_iff

theorem Sigma.lex_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) × α i}, Sigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (h ▸ a.snd) b.snd

This theorem states that for any types `ι` and `α`, where `α` is a type dependent on `ι`, and any relations `r` on `ι` and `s` on `α` dependent on `ι`, and any pairs `a` and `b` of type `ι` and `α` dependent on `ι`, the lexicographic order `Sigma.Lex` of `a` and `b` is equivalent to either `r` being true for the first elements of `a` and `b`, or there exists an equality between the first elements of `a` and `b` for which `s` holds for the second element of `a` (after substituting the equality) and the second element of `b`.

More concisely: For any type-dependent types `α: ι → Type`, relations `r: ι → ι → Prop` and `s: ι → α(ι) → α(ι) → Prop` on `ι` and `α` respectively, if `a` and `b` are pairs of type `(ι, α(ι))` such that `Sigma.Lex a < Sigma.Lex b` if and only if either `r a.0 b.0` holds or there exists an equality `a.0 = b.0` such that `s a.1 (a.0 = b.0) (a.1)` and `s b.1 (a.0 = b.0) (b.1)` hold.