sub_one_lt_floor

Mathlib.Algebra.Order.Floor.Semiring

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

English

For any a in a ring, a − 1 is strictly less than ⌊a⌋₊.

Русский

Для любого a в кольце верно a − 1 < ⌊a⌋₊.

LaTeX

$$$$ a - 1 < \\lfloor a \\rfloor_+ $$$$

Lean4

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

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

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

Разделы

Аффилиация

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