sub_half_lt_round

Mathlib.Algebra.Order.Round

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

← MathLib Explorer

English

For any x in α, x − 1/2 < round x.

Русский

Для любого x в α верно x − 1/2 < round x.

LaTeX

$$$\\\\forall x \\\\in \\alpha, \\\\; x - \\tfrac{1}{2} < \\\\operatorname{round} x.$$$

Lean4

@[bound]
theorem sub_half_lt_round (x : α) : x - 1 / 2 < round x :=
  by
  rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]
  exact Int.sub_one_lt_floor (x + 1 / 2)

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

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

Разделы

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

Аффилиация

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