English
The set ratLt(x) consists of rationals r whose numerator and denominator satisfy r.num·1 < r.den·x.
Русский
Множество ratLt(x) состоит из рациональных чисел r, для которых числитель и знаменатель удовлетворяют r.num·1 < r.den·x.
LaTeX
$$$\\text{ratLt}(x) = \\{ r \\in \\mathbb{Q} : r.\\mathrm{num} \\cdot 1 < r.\\mathrm{den} \\cdot x \\}. $$$
Lean4
/-- For `u v : ℚ` and `x y : M`, one can informally write
`u < x → v < y → u + v < x + y`. We formalize this using smul. -/
theorem num_smul_one_lt_den_smul_add {u v : ℚ} {x y : M} (hu : u.num • 1 < u.den • x) (hv : v.num • 1 < v.den • y) :
(u + v).num • 1 < (u + v).den • (x + y) :=
by
have hu' : (u.num * v.den) • 1 < (u.den * v.den : ℤ) • x := by
simpa [mul_comm] using (mul_smul_one_lt_iff v.den_pos).mpr hu
suffices ((u + v).num * u.den * v.den) • 1 < ((u + v).den : ℤ) • (u.den * v.den : ℤ) • (x + y)
by
refine (mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_
rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ), smul_assoc]
rw [Rat.add_num_den', mul_comm, ← smul_smul]
rw [smul_lt_smul_iff_of_pos_left (by simpa using (u + v).den_pos)]
rw [add_smul, smul_add]
exact add_lt_add hu' ((mul_smul_one_lt_iff u.den_pos).mpr hv)
