lt_of_ceil_lt

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.lt_of_ceil_lt

English

If ⌈a⌉₊ < n for some n ∈ ℕ, then a < n.

Русский

Если ⌈a⌉₊ < n для некоторого n ∈ ℕ, то a < n.

LaTeX

$$$$\text{If } \lceil a \rceil_{+} < n,\ \ a < n.$$$$

Lean4

theorem lt_of_ceil_lt (h : ⌈a⌉₊ < n) : a < n :=
  (le_ceil a).trans_lt (Nat.cast_lt.2 h)

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

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

Разделы

Аффилиация

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