lt_one_of_floor_lt_one

Mathlib.Algebra.Order.Floor.Semiring

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

English

If ⌊a⌋_+ < 1, then a < 1.

Русский

Если ⌊a⌋_+ < 1, тогда a < 1.

LaTeX

$$$$ h: \lfloor a \rfloor_+ < 1 \Rightarrow a < 1 $$$$

Lean4

theorem lt_one_of_floor_lt_one (h : ⌊a⌋₊ < 1) : a < 1 :=
  mod_cast lt_of_floor_lt h

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

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

Разделы

Аффилиация

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