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