ceil_nonneg_of_neg_one_lt

Mathlib.Algebra.Order.Floor.Ring

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

English

If -1 < a then 0 ≤ ⌈a⌉.

Русский

Если -1 < a, тогда 0 ≤ ⌈a⌉.

LaTeX

$$$-1 < a \\\\Rightarrow 0 \\\\le \\\\lceil a \rceil$$$

Lean4

theorem ceil_nonneg_of_neg_one_lt (ha : -1 < a) : 0 ≤ ⌈a⌉ := by rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]

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

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

Разделы

Аффилиация

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