floor_le_one_of_le_one

Mathlib.Algebra.Order.Floor.Semiring

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

English

If a ≤ 1 then ⌊a⌋₊ ≤ 1.

Русский

Если a ≤ 1, то ⌊a⌋₊ ≤ 1.

LaTeX

$$a \le 1 \Rightarrow \lfloor a \rfloor_+ \le 1$$

Lean4

theorem floor_le_one_of_le_one (h : a ≤ 1) : ⌊a⌋₊ ≤ 1 :=
  floor_le_of_le <| h.trans_eq <| Nat.cast_one.symm

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

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

Разделы

Аффилиация

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