invRev_bijective — Mathlib

English

The map invRev on words is bijective; in particular it is a bijection with an explicit inverse given by itself.

Русский

Отображение invRev над словами биективно; в частности оно имеет явное обратное, равное самому invRev.

LaTeX

$$$\\forall w:\\text{List}(\\alpha \\times \\mathsf{Bool}),\\ \\exists! v:\\text{List}(\\alpha \\times \\mathsf{Bool}), invRev(v)=w$$$

Lean4

@[to_additive]
theorem invRev_bijective : Function.Bijective (@invRev α) :=
  invRev_involutive.bijective

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