one_le_floor_iff

Mathlib.Algebra.Order.Floor.Semiring

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

English

The floor is positive exactly when a > 0, i.e., 0 < a ⇔ 0 < floor(a).

Русский

Положительность floor(a) эквивалентна тому, что a > 0: 0 < a ⇔ 0 < ⌊a⌋₊.

LaTeX

$$0 < \lfloor a \rfloor_+ \Longleftrightarrow 1 \le a$$

Lean4

@[simp]
theorem one_le_floor_iff (x : R) : 1 ≤ ⌊x⌋₊ ↔ 1 ≤ x :=
  mod_cast le_floor_iff' one_ne_zero

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

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

Разделы

Аффилиация

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