English
For any indexing, the Lex relation on Σ i, αi is characterized by: Lex r s a b holds iff ra1 b1 or there exists an equality a1=b1 with the second components related by s after transporting along that equality.
Русский
Для любых элементов Σ i, αi равенство Lex r s a b эквивалентно: Lex r s a b выполняется тогда и только тогда, когда r между первых координат выполняется или существует равенство первых координат a1=b1 и вторые координаты связаны через s после переноса вдоль этого равенства.
LaTeX
$$$\\operatorname{Lex} r s a b \\Leftrightarrow r a.1 b.1 \\;\\lor\\; \\exists h:a.1=b.1,\\, s b.1 (h.\\mathrm{rec} a.2) b.2$$$
Lean4
theorem lex_iff : 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⟩ | ⟨a, b, 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
