reverse_surjective — Mathlib

English

The reverse operation is surjective: for every list, there exists a preimage whose reverse is that list.

Русский

Операция разворота сюръективна: для каждого списка найдётся предобраз, чьим разворотом является данный список.

LaTeX

$$$$\\forall s:\\\\mathrm{List}\\\\alpha,\\\\ ∃ t:\\\\mathrm{List}\\\\alpha,\\\\ \\mathrm{reverse}(t) = s.$$$$

Lean4

theorem reverse_surjective : Surjective (@reverse α) :=
  reverse_involutive.surjective

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