floor_pos

Mathlib.Algebra.Order.Floor.Semiring

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

English

If n < floor(a) then n < a (in R).

Русский

Если n < ⌊a⌋₊, то n < a в R.

LaTeX

$$n < \lfloor a \rfloor_+ \Rightarrow (n : R) < a$$

Lean4

theorem floor_pos : 0 < ⌊a⌋₊ ↔ 1 ≤ a := by rw [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, cast_one]

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

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

Разделы

Аффилиация

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