invRev_cons — Mathlib

English

If you prepend a letter a to L, invRev behaves as invRev(L) concatenated with invRev([a]).

Русский

Если приписать букву a к L слева, то invRev ведёт себя как invRev(L) конкатенированное с invRev([a]).

LaTeX

$$$\mathrm{invRev}(a \;::\; L) = \mathrm{invRev}(L) \;\Vert\; \mathrm{invRev}([a]).$$$

Lean4

@[to_additive]
theorem invRev_cons {a : (α × Bool)} : invRev (a :: L) = invRev L ++ invRev [a] := by simp [invRev]

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