fract_add — Mathlib

English

Let a,b be elements of a linearly ordered ring with a floor function. Then there exists an integer z such that fract(a+b) = fract(a) + fract(b) + z.

Русский

Пусть a,b ∈ R, где R — упорядоченное кольцо с функцией floor. Тогда существует целое z такое, что fract(a+b) = fract(a) + fract(b) + z.

LaTeX

$$$\exists z \in \mathbb{Z}, \operatorname{fract}(a+b) = \operatorname{fract}(a) + \operatorname{fract}(b) + z$$$

Lean4

theorem fract_add (a b : R) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
  ⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by unfold fract; grind⟩

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