abs_sub_round

Mathlib.Algebra.Order.Round

URI: https://scilib.ai/kg/mathlib#abs_sub_round

← MathLib Explorer

English

For any α, |x − round x| ≤ 1/2.

Русский

Для любого x из поля выполняется |x − round x| ≤ 1/2.

LaTeX

$$$\\\\left|x - \\\\operatorname{round} x\\\\right| \\\\le \\\\tfrac{1}{2}.$$$

Lean4

theorem abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 :=
  by
  rw [round_eq, abs_sub_le_iff]
  have := floor_le (x + 1 / 2)
  have := lt_floor_add_one (x + 1 / 2)
  constructor <;> linarith

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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