abs_one_sub_fract

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.abs_one_sub_fract

English

0 ≤ fract a < 1.

Русский

0 ≤ fract(a) < 1.

LaTeX

$$0 \leq \operatorname{fract}(a) < 1$$

Lean4

@[simp]
theorem abs_one_sub_fract : |1 - fract a| = 1 - fract a :=
  abs_eq_self.mpr <| sub_nonneg.mpr (fract_lt_one a).le

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru