floor_le_floor

Mathlib.Algebra.Order.Floor.Semiring

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

English

If a ≤ b then floor(a) ≤ floor(b).

Русский

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

LaTeX

$$($a \le b) \Rightarrow (\lfloor a \rfloor_+ \le \lfloor b \rfloor_+$)$$

Lean4

@[gcongr, bound]
theorem floor_le_floor (hab : a ≤ b) : ⌊a⌋₊ ≤ ⌊b⌋₊ :=
  floor_mono hab

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

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

Разделы

Аффилиация

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