floor_nonneg

Mathlib.Algebra.Order.Floor.Defs

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

English

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

Русский

0 ≤ ⌊a⌋ тогда и только тогда, когда 0 ≤ a.

LaTeX

$$$0 \le \lfloor a \rfloor \iff 0 \le a.$$$

Lean4

theorem floor_nonneg : 0 ≤ ⌊a⌋ ↔ 0 ≤ a := by rw [le_floor, Int.cast_zero]

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

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

Разделы

Аффилиация

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