lower_raise' — Mathlib

English

For any l and n, applying lower' to l with n and then raise' to the result recovers the original list: raise'(lower'(l,n), n) = l.

Русский

Для любых l и n применение lower' к l с параметром n, затем raise' к результату возвращает исходный список: raise'(lower'(l,n), n) = l.

LaTeX

$$$\forall l\,n,\, \text{raise'}(\text{lower'}(l,n), n) = l$$$

Lean4

theorem lower_raise' : ∀ l n, lower' (raise' l n) n = l
  | [], _ => rfl
  | m :: l, n => by simp [raise', lower', lower_raise']

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