A bound for the first sixty-four reciprocals
ProvedWorkbookSyntax.plus_40974lean-workbookrepaired-notationsource-checked
.
Notation repair: Replaced the obsolete finite-sum binder “in” with the current “∈” notation. The ranges, summands, hypotheses and conclusion are unchanged.
Source: Lean-Workbook record lean_workbook_plus_40974 (Apache-2.0). Original declaration.
Preamble
import Mathlib open Nat
Formal statement
theorem WorkbookSyntax.plus_40974 : ∑ i ∈ Finset.Icc (1 : ℕ) 64, (1 : ℝ) / i < 6.4 := by sorry
Source