round_sub_ofNat — Mathlib

English

If n ≥ 2 is a natural number, then round(x − ofNat(n)) = round(x) − ofNat(n).

Русский

Если n ≥ 2 — натуральное число, то round(x − ofNat(n)) = round(x) − ofNat(n).

LaTeX

$$$\\\\forall x \in \\alpha, \\\\\\forall n \\in \\mathbb{N}, [n \\ge 2] \\\\\\operatorname{round}(x - \\operatorname{ofNat}(n)) = \\\\\\operatorname{round}(x) - \\operatorname{ofNat}(n).$$$

Lean4

@[simp]
theorem round_sub_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] : round (x - ofNat(n)) = round x - ofNat(n) :=
  round_sub_natCast x n

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