le_floorDiv_iff_smul_le

Mathlib.Algebra.Order.Floor.Div

URI: https://scilib.ai/kg/mathlib#le_floorDiv_iff_smul_le

English

For a > 0, c ≤ b ⌊/⌋ a is equivalent to a ⋅ c ≤ b.

Русский

Пусть a > 0. Тогда c ≤ b ⌊/⌋ a эквивалентно a ⋅ c ≤ b.

LaTeX

$$$ ha > 0 \\\\Rightarrow \\\\bigl( c \\\\le b \\\\ll floor / a \\\\rr) \\\\Leftrightarrow \\\\bigl( a \\\\cdot c \\\\le b \\\\bigr).$$$

Lean4

@[simp]
theorem le_floorDiv_iff_smul_le (ha : 0 < a) : c ≤ b ⌊/⌋ a ↔ a • c ≤ b :=
  (gc_floorDiv_smul ha _ _).symm

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

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

Разделы

Аффилиация

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