Uniform convergence of x/n on ball(0,1) using filter

Stream: mathlib4

[Daniel Eriksson]

I am trying to understand the definition of uniform convergence using filters in Mathlib by the showing the following simple example.

lemma xdivn_conv_unif_ball01: TendstoUniformlyOn
(fun (n:ℕ) (x:ℝ) ↦ x/(n+1)) (fun (x:ℝ)↦ 0) atTop
      (ball 0 1) := by
intro u h
sorry

Given a filter U in $\mathbb R\times \mathbb R$, I want to find a filter ${n≤N}$,or $N\in \N$, so that $A_N=\{(0,x/n):x\in ball(0,1),n\leq N\} \in U$. But $A_N=A_0$ for all N so I am not sure if I am right?

[Luigi Massacci]

For this kind of concrete goal, you are better off switching to the metric language early I think, you don't really gain anything from filters

[Luigi Massacci]

Here is one possible proof:

import Mathlib

open Filter Metric

lemma xdivn_conv_unif_ball01: TendstoUniformlyOn (fun (n:ℕ) (x:ℝ) ↦ x/n) 0 atTop (ball 0 1) := by
  refine SeminormedAddGroup.tendstoUniformlyOn_zero.mpr (fun ε εpos ↦ eventually_atTop.mpr ?_)
  obtain ⟨n, npos, hn⟩ := Real.exists_nat_pos_inv_lt εpos
  refine ⟨n, fun m hm x hx ↦ ?_⟩
  have : |x| < 1 := Real.norm_eq_abs x ▸ (mem_ball_zero_iff.mp hx)
  rw [norm_div, Real.norm_eq_abs, Real.norm_natCast]
  calc
    _ ≤ |x| / n := by gcongr
    _ ≤ 1 / (n : ℝ) := by gcongr
    _ < ε := by simp only [one_div, hn]

[Daniel Eriksson]

Ah good suggestion, many thanks!