English
There exists an order isomorphism between the lexicographic sum of the right and left sub-relations and the original relation r, with toEquiv given by a composition of Equiv.sumComm and sumCompl.
Русский
Существует упорядоченный изоморфизм между лексикографической суммой правой и левой части подотношений и исходным отношением r, с отображением toEquiv = (Equiv.sumComm).trans (Equiv.sumCompl (r x)).
LaTeX
$$$\\mathrm{sumLexComplRight} : \\mathrm{Sum.Lex}(\\mathrm{Subrel}(r, \\neg r x·))(\\mathrm{Subrel}(r, r x)) \\cong_r r$$$
Lean4
/-- A relation is isomorphic to the lexicographic sum of elements not greater than `x` and elements
greater than `x`. -/
def sumLexComplRight : Sum.Lex (Subrel r (¬r x ·)) (Subrel r (r x)) ≃r r
where
toEquiv := (Equiv.sumComm _ _).trans <| .sumCompl (r x)
map_rel_iff' := by
rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)
· simp
· simpa using trans_trichotomous_left ha hb
· simpa using fun h ↦ hb <| trans ha h
· simp
