reverse_eq_image — Mathlib

English

The reverse of a language equals the image of the reverse map on the language: l.reverse = List.reverse '' l.

Русский

Обратный образ языка равен образу операции разворота списка на языке: l.reverse = List.reverse '' l.

LaTeX

$$l.reverse = \\mathrm{List}.reverse '' l$$

Lean4

theorem reverse_eq_image (l : Language α) : l.reverse = List.reverse '' l :=
  ((List.reverse_involutive.toPerm _).image_eq_preimage _).symm

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