English
There is an order isomorphism between nested sums: (α ⊕ β) ⊕ γ ≃o α ⊕ (β ⊕ γ), given by sumAssoc.
Русский
Существует упорядоченный преобразователь между двумя способом ассоциирования суммы: (α ⊕ β) ⊕ γ ≃o α ⊕ (β ⊕ γ), задаваемый sumAssoc.
LaTeX
$$$\text{sumAssoc }(\alpha,\beta,\gamma) : (\alpha \oplus \beta) \oplus \gamma \;\cong_o\; \alpha \oplus (\beta \oplus \gamma)$$$
Lean4
/-- `Equiv.sumAssoc` promoted to an order isomorphism. -/
def sumAssoc (α β γ : Type*) [LE α] [LE β] [LE γ] : (α ⊕ β) ⊕ γ ≃o α ⊕ (β ⊕ γ) :=
{ Equiv.sumAssoc α β γ with
map_rel_iff' := fun {a b} => by
rcases a with ((_ | _) | _) <;> rcases b with ((_ | _) | _) <;> simp [Equiv.sumAssoc] }
