invRev_append — Mathlib

English

Inverse of a concatenation reverses the order of the inverses: invRev(L1 ++ L2) = invRev(L2) ++ invRev(L1).

Русский

Обратное от конкатенации разворачивает порядок обратных: invRev(L1 ++ L2) = invRev(L2) ++ invRev(L1).

LaTeX

$$$\mathrm{invRev}(L_1 \;\Vert\; L_2) = \mathrm{invRev}(L_2) \;\Vert\; \mathrm{invRev}(L_1).$$$

Lean4

@[to_additive (attr := simp)]
theorem invRev_append : invRev (L₁ ++ L₂) = invRev L₂ ++ invRev L₁ := by simp [invRev]

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