(err : ℕ → ℝ) (C Dmin h nv : ℝ) (hh : 0 < h) (hnn : ∀ m, 0 ≤ err m) (hle : ∀ m, err m ≤ sirkBound C Dmin h nv m) : Tendsto err atTop (𝓝 0)

Initializing...

(err : ℕ → ℝ) (C Dmin h nv : ℝ) (hh : 0 < h) (hnn : ∀ m, 0 ≤ err m) (hle : ∀ m, err m ≤ sirkBound C Dmin h nv m) : Tendsto err atTop (𝓝 0) · Prove2Me