lt_floor_iff

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.lt_floor_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

theorem lt_floor_iff : z < ⌊a⌋ ↔ z + 1 ≤ a := by rw [← add_one_le_iff, le_floor]; norm_cast

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

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

Разделы

Аффилиация

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