toDegLex_symm_eq — Mathlib

English

The inverse of the canonical map toDegLex is exactly the map ofDegLex; i.e., toDegLex is the inverse of the equivalence given by ofDegLex.

Русский

Обратное отображение к каноническому отображению toDegLex равно отображению ofDegLex; то есть toDegLex является обратным отображением эквивалентности, заданной через ofDegLex.

LaTeX

$$$(toDegLex)^{-1} = ofDegLex$$$

Lean4

@[simp]
theorem toDegLex_symm_eq : (@toDegLex α).symm = ofDegLex :=
  rfl

Похожие утверждения