English
For PSigma with PSigma.lex, Lex r s a b holds iff r a.1 b.1 or there exists h: a.1 = b.1 with s b.1 (h.rec a.2) b.2.
Русский
Для PSigma.Lex лексическое отношение на PSigma выражается как: Lex r s a b выполняется тогда и только тогда, когда r a.1 b.1 или существует h: a.1 = b.1, причём s b.1 (h.rec a.2) b.2.
LaTeX
$$$\\text{PSigma.lex\\_iff}:\\; \\mathrm{Lex}\\ r\\ s\\ a\\ b \\iff r\\ a.1\\ b.1 \\lor \\exists h: a.1 = b.1, s\\ b.1 (\\mathrm{Eq.rec}\\ a.2\\ h) b.2$$$
Lean4
theorem lex_iff {a b : Σ' i, α i} : Lex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec a.2) b.2 :=
by
constructor
· rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
· exact Or.inl hij
· exact Or.inr ⟨rfl, hab⟩
· obtain ⟨i, a⟩ := a
obtain ⟨j, b⟩ := b
dsimp only
rintro (h | ⟨rfl, h⟩)
· exact Lex.left _ _ h
· exact Lex.right _ h
