sub_one_lt_floor

Mathlib.Algebra.Order.Floor.Ring

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

English

For all a ∈ R, a − 1 < ⌊a⌋.

Русский

Для любого a ∈ R верно: a − 1 < ⌊a⌋.

LaTeX

$$$$ a - 1 < \\lfloor a \\rfloor $$$$

Lean4

@[simp, bound]
theorem sub_one_lt_floor (a : R) : a - 1 < ⌊a⌋ :=
  sub_lt_iff_lt_add.2 (lt_floor_add_one a)

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

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

Разделы

Аффилиация

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