floor_eq_zero

Mathlib.Algebra.Order.Floor.Semiring

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

English

The floor is zero exactly when a < 1.

Русский

Этаж равен нулю тогда и только тогда, когда a < 1.

LaTeX

$$\lfloor a \rfloor_+ = 0 \iff a < 1$$

Lean4

@[simp]
theorem floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1 :=
  by
  rw [← lt_one_iff, ← @cast_one R]
  exact floor_lt' Nat.one_ne_zero

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

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

Разделы

Аффилиация

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