ofDegLex_symm_eq — Mathlib

English

Let f be the isomorphism between α and DegLex(α) given by ofDegLex, and g its inverse given by toDegLex. Then f and g are inverse bijections; equivalently, the inverse of f is g, and f is invertible with g as its inverse.

Русский

Пусть f: α → DegLex(α) — отображение, заданное как ofDegLex, и g: DegLex(α) → α — его обратное отображение toDegLex. Тогда f и g являются взаимно однозначными обратимыми отображениями; эквивалентно: обратное отображение к f равно g, и f имеет обратное g.

LaTeX

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

Lean4

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

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