English
A repeated transitivity property for sumLexCongr as in the previous item.
Русский
Повторение свойства транспозиции sumLexCongr.
LaTeX
$$$\text{(repeat)}$$$
Lean4
/-- `Equiv.sumAssoc` promoted to an order isomorphism. -/
def sumLexAssoc (α β γ : Type*) [LE α] [LE β] [LE γ] : (α ⊕ₗ β) ⊕ₗ γ ≃o α ⊕ₗ β ⊕ₗ γ :=
{ Equiv.sumAssoc α β γ with
map_rel_iff' := fun {a b} =>
⟨fun h =>
match a, b, h with
| inlₗ (inlₗ _), inlₗ (inlₗ _), Lex.inl h => Lex.inl <| Lex.inl h
| inlₗ (inlₗ _), inlₗ (inrₗ _), Lex.sep _ _ => Lex.inl <| Lex.sep _ _
| inlₗ (inlₗ _), inrₗ _, Lex.sep _ _ => Lex.sep _ _
| inlₗ (inrₗ _), inlₗ (inrₗ _), Lex.inr (Lex.inl h) => Lex.inl <| Lex.inr h
| inlₗ (inrₗ _), inrₗ _, Lex.inr (Lex.sep _ _) => Lex.sep _ _
| inrₗ _, inrₗ _, Lex.inr (Lex.inr h) => Lex.inr h,
fun h =>
match a, b, h with
| inlₗ (inlₗ _), inlₗ (inlₗ _), Lex.inl (Lex.inl h) => Lex.inl h
| inlₗ (inlₗ _), inlₗ (inrₗ _), Lex.inl (Lex.sep _ _) => Lex.sep _ _
| inlₗ (inlₗ _), inrₗ _, Lex.sep _ _ => Lex.sep _ _
| inlₗ (inrₗ _), inlₗ (inrₗ _), Lex.inl (Lex.inr h) => Lex.inr <| Lex.inl h
| inlₗ (inrₗ _), inrₗ _, Lex.sep _ _ => Lex.inr <| Lex.sep _ _
| inrₗ _, inrₗ _, Lex.inr h => Lex.inr <| Lex.inr h⟩ }
