of_inv_fr_num_lt_num_of_pos — Mathlib

English

For any q > 0 with q < 1, the numerator of the fractional part of IntFractPair.of q⁻¹ is smaller than that of q.

Русский

Для любого q > 0 с q < 1 числитель дробной части IntFractPair.of q⁻¹ меньше числителя q.

LaTeX

$$∀ q with 0 < q < 1, (IntFractPair.of q⁻¹).fr.num < q.num$$

Lean4

/-- Shows that for any `q : ℚ` with `0 < q < 1`, the numerator of the fractional part of
`IntFractPair.of q⁻¹` is smaller than the numerator of `q`.
-/
theorem of_inv_fr_num_lt_num_of_pos (q_pos : 0 < q) : (IntFractPair.of q⁻¹).fr.num < q.num :=
  Rat.fract_inv_num_lt_num_of_pos q_pos

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