truncate_approx — Mathlib

English

The truncate operation reduces the height of an approximation by one level: truncate(x.approx (n+1)) = x.approx n.

Русский

Операция truncate уменьшает высоту аппроксимации на один уровень: truncate(x.approx (n+1)) = x.approx n.

LaTeX

$$$\\operatorname{truncate}\\bigl( x.approx(\\operatorname{succ} n) \\bigr) = x.approx n$$$

Lean4

theorem truncate_approx (x : M F) (n : ℕ) : truncate (x.approx <| n + 1) = x.approx n :=
  truncate_eq_of_agree _ _ (x.consistent _)

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