reverse_injective — Mathlib

English

The reverse operation on context-free grammars is injective; distinct grammars map to distinct reverses.

Русский

Операция разворота над грамматиками инъективна; разные грамматики имеют разные развороты.

LaTeX

$$$ \mathrm{Injective}(\mathrm{reverse}) $$$

Lean4

theorem reverse_injective : Injective (reverse : ContextFreeGrammar T → ContextFreeGrammar T) :=
  reverse_bijective.injective

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