mabs_div_le_of_one_le_of_le — Mathlib

English

1 ≤ a ≤ n and 1 ≤ b ≤ n imply |a/b|_m ≤ n.

Русский

1 ≤ a ≤ n и 1 ≤ b ≤ n предполагают |a/b|_м ≤ n.

LaTeX

$$$1 \le a \le n \land 1 \le b \le n \implies \left|\frac{a}{b}\right|_m \le n$$$

Lean4

/-- `|a / b|ₘ ≤ n` if `1 ≤ a ≤ n` and `1 ≤ b ≤ n`. -/
@[to_additive /-- `|a - b| ≤ n` if `0 ≤ a ≤ n` and `0 ≤ b ≤ n`. -/
    ]
theorem mabs_div_le_of_one_le_of_le {a b n : G} (one_le_a : 1 ≤ a) (a_le_n : a ≤ n) (one_le_b : 1 ≤ b)
    (b_le_n : b ≤ n) : |a / b|ₘ ≤ n :=
  by
  rw [mabs_div_le_iff, div_le_iff_le_mul, div_le_iff_le_mul]
  exact ⟨le_mul_of_le_of_one_le a_le_n one_le_b, le_mul_of_le_of_one_le b_le_n one_le_a⟩

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