le_floorDiv_iff_mul_le

Mathlib.Algebra.Order.Floor.Div

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

English

For a > 0, c ≤ b ⌊/⌋ a iff a • c ≤ b.

Русский

Для a > 0, c ≤ b ⌊/⌋ a эквивалентно a • c ≤ b.

LaTeX

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

Lean4

theorem le_floorDiv_iff_mul_le (ha : 0 < a) : c ≤ b ⌊/⌋ a ↔ a • c ≤ b :=
  le_floorDiv_iff_smul_le ha

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

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

Разделы

Аффилиация

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