lean_workbook_plus_62007
Disprovedwe get that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62007 : ∀ n : ℕ, ∀ a : ℝ, (1 + a / (n + 1)) ^ (n + 1) > (1 + a / n) ^ n := by sorry
Source
we get that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_62007 : ∀ n : ℕ, ∀ a : ℝ, (1 + a / (n + 1)) ^ (n + 1) > (1 + a / n) ^ n := by sorry