toColex_symm_eq — Mathlib

English

There exists a bijective correspondence between α and Colex α, with inverse given by the map ofColex; equivalently, the inverse of toColex is ofColex.

Русский

Существует биекция между множеством α и Colex α, обратная к которой задаётся отображением ofColex; эквивалентно, обратное отображение к toColex равно toColex.

LaTeX

$$$(to\\!\\circ\\!of)_{Colex} = \\mathrm{id}_{Colex\\,\\alpha} \\land (of\\!\\circ\\!to)_{\\alpha} = \\mathrm{id}_{\\alpha}$$$

Lean4

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

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