English
The set of rationals below x+y equals the sum of the sets below x and below y.
Русский
Множество рациональных чисел, меньшее x+y, совпадает с суммой множеств рационалов, меньших x и меньших y.
LaTeX
$$$\operatorname{ratLt}(x+y) = \operatorname{ratLt}(x) + \operatorname{ratLt}(y)$$$
Lean4
theorem ratLt_add (x y : M) : ratLt (x + y) = ratLt x + ratLt y :=
by
ext a
rw [Set.mem_add]
constructor
· /- Given `a ∈ ratLt 1 (x + y)`, find `u ∈ ratLt 1 x`, `v ∈ ratLt 1 y`
such that `u + v = a`.
In a naive attempt, one can take the denominator `d` of `a`,
and find the largest `u = p / d < x / 1`.
However, `d` could be too "coarse", and `v = a - u` could be 1/d too large than `y / 1`.
To ensure a large enough denominator, we take `d * k`, where
`1 + 1 ≤ k • (d • (x + y) - a.num • 1)`. -/
intro h
rw [Set.mem_setOf_eq] at h
obtain ⟨k, hk⟩ := Archimedean.arch (1 + 1) <| sub_pos.mpr h
have hk0 : k ≠ 0 := by
contrapose! hk
simp [hk]
have hka0 : k * a.den ≠ 0 := mul_ne_zero hk0 a.den_ne_zero
obtain ⟨m, ⟨hm1, hm2⟩, _⟩ := existsUnique_add_zsmul_mem_Ico zero_lt_one 0 (k • a.den • x - 1)
refine ⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.den), ?_, ?_⟩
· rw [mkRat_mem_ratLt hka0, ← smul_smul]
simpa using hm2
· have hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1 :=
by
rw [smul_add, smul_sub, smul_add, le_sub_iff_add_le, ← sub_le_iff_le_add] at hk
rw [le_sub_iff_add_le]
convert hk using 1
abel
have : k • a.num • 1 - k • a.den • y < m • 1 :=
lt_of_lt_of_le (lt_add_of_pos_left _ zero_lt_one) (by simpa using hk'.trans hm1)
rw [mkRat_mem_ratLt hka0, sub_smul, sub_lt_comm, ← smul_smul, ← smul_smul, natCast_zsmul]
exact this
· rw [Rat.mkRat_add_mkRat_of_den _ _ hka0]
rw [add_sub_cancel, Rat.mkRat_mul_left hk0, Rat.mkRat_num_den']
· -- `u ∈ ratLt 1 x`, `v ∈ ratLt 1 y` → `u + v ∈ ratLt 1 (x + y)`
intro ⟨u, hu, v, hv, huv⟩
rw [← huv]
rw [Set.mem_setOf_eq] at hu hv ⊢
exact num_smul_one_lt_den_smul_add hu hv
