reverse_bijective — Mathlib

English

For any type α, the reverse operation on lists is a bijection from List α to List α.

Русский

Для любого типа α операция разворота списка является биекцией на множества списков α.

LaTeX

$$$\\\\mathrm{Bijective}(\\\\mathrm{reverse} : \\\\mathrm{List}(\\\\alpha) \\\\to \\\\mathrm{List}(\\\\alpha))$$$

Lean4

theorem reverse_bijective : Bijective (@reverse α) :=
  reverse_involutive.bijective

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