floor_le_sub_one_iff

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.floor_le_sub_one_iff

English

For all a ∈ R and z ∈ ℤ, ⌊a⌋ ≤ z − 1 if and only if a < z.

Русский

Для любых a ∈ R и z ∈ ℤ верно: ⌊a⌋ ≤ z − 1 ⇔ a < z.

LaTeX

$$$$ \\lfloor a \\rfloor \\le z - 1 \\iff a < z $$$$

Lean4

@[simp]
theorem floor_le_sub_one_iff : ⌊a⌋ ≤ z - 1 ↔ a < z := by rw [← floor_lt, le_sub_one_iff]

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

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

Разделы

Аффилиация

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