invRev_surjective — Mathlib

English

Let α be a type. The operation invRev on words (lists of pairs from α×Bool) is surjective; in fact invRev is an involution, so every word has a preimage under invRev.

Русский

Пусть α — множество. Операция 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_surjective : Function.Surjective (@invRev α) :=
  invRev_involutive.surjective

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