truncate_mk' — Mathlib

English

For any f: ℕ → R, truncate n (@mk' p _ f) = TruncatedWittVector.mk p (fun k => f k).

Русский

Для любой f: ℕ → R, усечение n от @mk' p _ f равно TruncatedWittVector.mk p (fun k => f k).

LaTeX

$$$$\\operatorname{truncate}_n\\bigl(\\operatorname{mk}' p _ f\\bigr) = \\operatorname{TruncatedWittVector.mk} p\\, (\\lambda k. f\\, k). $$$$

Lean4

@[simp]
theorem truncate_mk' (f : ℕ → R) : truncate n (@mk' p _ f) = TruncatedWittVector.mk _ fun k => f k :=
  by
  ext i
  simp only [coeff_truncate, TruncatedWittVector.coeff_mk]

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