floor_pos

Mathlib.Algebra.Order.Floor.Ring

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

English

0 < ⌊a⌋ if and only if 1 ≤ a.

Русский

0 < ⌊a⌋ ⇔ 1 ≤ a.

LaTeX

$$$$ 0 < \\lfloor a \\rfloor \\iff 1 \\le a $$$$

Lean4

theorem floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a := by rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]

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

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

Разделы

Аффилиация

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