lt_succ_floor

Mathlib.Algebra.Order.Floor.Ring

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

English

For any a ∈ R, a < ⌊a⌋.succ.

Русский

Для произвольного a ∈ R верно: a < ⌊a⌋.succ.

LaTeX

$$$$ a < \\lfloor a \\rfloor .\\text{succ} $$$$

Lean4

theorem lt_succ_floor (a : R) : a < ⌊a⌋.succ :=
  floor_lt.1 <| Int.lt_succ_self _

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

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

Разделы

Аффилиация

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