English
If r is irrational, the positive Beatty sequences for beattySeq' r and beattySeq r coincide: {beattySeq' r k | k > 0} = {beattySeq r k | k > 0}.
Русский
Если r иррационально, то положительные последовательности BeattyBeattySeq' и BeattySeq совпадают.
LaTeX
$$$\\{beattySeq' r k \\;|\\; k>0\\} = \\{beattySeq r k \\;|\\; k>0\\}$$$
Lean4
/-- Let `r` be an irrational number. Then `B⁺_r` and `B⁺'_r` are equal. -/
theorem beattySeq'_pos_eq {r : ℝ} (hr : Irrational r) : {beattySeq' r k | k > 0} = {beattySeq r k | k > 0} :=
by
dsimp only [beattySeq, beattySeq']
congr! 4; rename_i k; rw [and_congr_right_iff]; intro hk; congr!
rw [sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one, add_sub_cancel_right]
refine ⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩
exact (hr.intCast_mul hk.ne').ne_int ⌊k * r⌋ h.symm
