le_of_ceil_le

Mathlib.Algebra.Order.Floor.Semiring

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

English

Let a ∈ R and n ∈ ℕ. If the ceiling of a satisfies ⌈a⌉ ≤ n, then a ≤ n.

Русский

Пусть a ∈ R и n ∈ ℕ. Если ⌈a⌉ ≤ n, то a ≤ n.

LaTeX

$$$\lceil a \rceil \le n \Rightarrow a \le n$$$

Lean4

theorem le_of_ceil_le (h : ⌈a⌉₊ ≤ n) : a ≤ n :=
  (le_ceil a).trans (Nat.cast_le.2 h)

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

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

Разделы

Аффилиация

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