ofColex_symm_eq — Mathlib

English

The inverse of the inverse map of Colex is the original map toColex; equivalently, the inverse of ofColex is toColex.

Русский

Обратное отображение к отображению обратной Colex есть исходное отображение toColex; эквивалентно, обратное отображение к ofColex равно toColex.

LaTeX

$$$(ofColex\\circ toColex) = \\mathrm{id}_{α}$$$

Lean4

@[simp]
theorem ofColex_symm_eq : (@ofColex α).symm = toColex :=
  rfl

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