English
Let α and β be types with a semiring structure on α and a module action on β. The canonical Lex-linear equivalence between α and β is involutive in the sense that its inverse equals the canonical Lex-linear equivalence in the opposite direction. In particular, the inverse of the Lex-linear equivalence of α and β is the Lex-linear equivalence from α to β.
Русский
Пусть α и β — множества с полугруппой по Лексу и модульным действием, соответствующим образом. Каноническое лексикографическое линейное отображение между α и β обладает свойством, что его обратное отображение совпадает с каноническим лексикографическим линейным отображением от α к β.
LaTeX
$$$ (\operatorname{ofLexLinearEquiv} \alpha \beta)^{-1} = \operatorname{toLexLinearEquiv} \alpha \beta $$$
Lean4
@[simp]
theorem symm_ofLexLinearEquiv : (ofLexLinearEquiv α β).symm = toLexLinearEquiv α β :=
rfl
