English
If a natural-valued property p holds on an arithmetic progression n a + k for all k < n, then p holds frequently on all large natural arguments.
Русский
Если для произвольного n>0 свойство p выполняется на всех прогрессиях n a + k, тогда p часто выполняется для больших a.
LaTeX
$$$\forall p: \mathbb{N} \to \text{Prop}, \forall n>0, (\forall k < n, \forall^{\infty} a, p(n a + k)) \Rightarrow \forall^{\infty} a, p(a)$$$
Lean4
theorem atTop_of_arithmetic {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) (hp : ∀ k < n, ∀ᶠ a in atTop, p (n * a + k)) :
∀ᶠ a in atTop, p a := by
simp only [eventually_atTop] at hp ⊢
choose! N hN using hp
refine ⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩
rw [← Nat.div_add_mod b n]
have hlt := Nat.mod_lt b hn.bot_lt
refine hN _ hlt _ ?_
rw [ge_iff_le, Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]
exact (Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb
