round_le_add_half

Mathlib.Algebra.Order.Round

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

English

round x ≤ x + 1/2 for all x in α.

Русский

round x ≤ x + 1/2 для всех x в α.

LaTeX

$$$\\\\forall x \\\\in \\alpha, \\\\operatorname{round}(x) \\\\le x + \\tfrac{1}{2}.$$$

Lean4

@[bound]
theorem round_le_add_half (x : α) : round x ≤ x + 1 / 2 :=
  by
  rw [round_eq x]
  exact Int.floor_le (x + 1 / 2)

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

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

Разделы

Аффилиация

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