English
Let α, β, γ be types with a compatible order. The natural associativity isomorphism sumLexAssoc: α ⊕ₗ (β ⊕ₗ γ) ≃o (α ⊕ₗ β) ⊕ₗ γ identifies the two different ways of parenthesizing a triple sum in lexicographic order. In particular, its inverse sends inl a to inl (inl a) for all a ∈ α, i.e. (sumLexAssoc α β γ).symm (inl a) = inl (inl a).
Русский
Пусть α, β, γ — типы с упорядочиванием. Естественный изоморфизм порядка sumLexAssoc: α ⊕ₗ (β ⊕ₗ γ) ≃o (α ⊕ₗ β) ⊕ₗ γ определяет ассоциативность лексикографического сложения тройки. В частности, его обратный отображение отправляет inl a в inl (inl a) для любого a ∈ α, то есть (sumLexAssoc α β γ).symm (inl a) = inl (inl a).
LaTeX
$$$\\bigl(\\text{sumLexAssoc}_{\\alpha,\\beta,\\gamma}\\bigr)^{-1}(\\mathrm{inl}(a)) = \\mathrm{inl}(\\mathrm{inl}(a))$$$
Lean4
@[simp]
theorem sumLexAssoc_symm_apply_inl : (sumLexAssoc α β γ).symm (inl a) = inl (inl a) :=
rfl
