lt_of_floor_lt

Mathlib.Algebra.Order.Floor.Semiring

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

English

If ⌊a⌋ < n, then a < n.

Русский

Если ⌊a⌋ < n, то a < n.

LaTeX

$$$$ \text{Given } h: \lfloor a \rfloor_+ < n, \; a < n. $$$$

Lean4

theorem lt_of_floor_lt (h : ⌊a⌋₊ < n) : a < n :=
  lt_of_not_ge fun h' => (le_floor h').not_gt h

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

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

Разделы

Аффилиация

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