lt_ceil

Mathlib.Algebra.Order.Floor.Defs

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

English

For all a ∈ α and z ∈ ℤ, z < ⌈a⌉ iff z.cast < a.

Русский

Для любых a ∈ α и z ∈ ℤ, z < ⌈a⌉ тогда и только тогда, когда z.cast < a.

LaTeX

$$$\forall a \in \alpha, \forall z \in \mathbb{Z},\; z < \lceil a \rceil \iff (z) < a.$$$

Lean4

theorem lt_ceil : z < ⌈a⌉ ↔ (z : α) < a :=
  lt_iff_lt_of_le_iff_le ceil_le

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

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

Разделы

Аффилиация

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