floor_lt_one

Mathlib.Algebra.Order.Floor.Semiring

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

English

For ha: 0 ≤ a, we have ⌊a⌋_+ < 1 if and only if a < 1.

Русский

Для ha: 0 ≤ a верно, что ⌊a⌋_+ < 1 тогда и только тогда, когда a < 1.

LaTeX

$$$$ ha: 0 \le a \Rightarrow \lfloor a \rfloor_+ < 1 \iff a < 1 $$$$

Lean4

theorem floor_lt_one (ha : 0 ≤ a) : ⌊a⌋₊ < 1 ↔ a < 1 :=
  (floor_lt ha).trans <| by rw [Nat.cast_one]

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

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

Разделы

Аффилиация

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