Even stronger statement

Changes

1 changed files (+1/-1)

• Analysis.lean
  • @@ -1,6 +1,6 @@
    import Mathlib - example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x < 1 / n) : x = 0 := by + example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x ≤ 1 / n) : x = 0 := by by_contra have := hn <| Nat.ceil (2 / x) have : x > 1 / (Nat.ceil (2 / x)) := by