truncateFun_sub — Mathlib

English

truncateFun n preserves subtraction: truncateFun n (x - y) = truncateFun n x - truncateFun n y.

Русский

Усечение сохраняет вычитание: truncateFun n (x - y) = truncateFun n x - truncateFun n y.

LaTeX

$$$ \operatorname{truncateFun}(n)(x - y) = \operatorname{truncateFun}(n)(x) - \operatorname{truncateFun}(n)(y) $$$

Lean4

theorem truncateFun_sub (x y : 𝕎 R) : truncateFun n (x - y) = truncateFun n x - truncateFun n y := by
  witt_truncateFun_tac

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