one_le_ceil_iff

Mathlib.Algebra.Order.Floor.Ring

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

English

1 ≤ ⌈a⌉ if and only if 0 < a.

Русский

1 ≤ ⌈a⌉ если и только если 0 < a.

LaTeX

$$$1 \\\\le \\\\lceil a \\\rceil \\\\iff 0 < a$$$

Lean4

@[simp]
theorem one_le_ceil_iff : 1 ≤ ⌈a⌉ ↔ 0 < a := by rw [← zero_add (1 : ℤ), add_one_le_ceil_iff, cast_zero]

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

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

Разделы

Аффилиация

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