lean_workbook_plus_43025
ProvedFor we have and , so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43025 (x : ℕ → ℝ) (hx: ∀ n, 1 <= x n ∧ x n <= 2) : ∀ n, x n ^ 3 + 1 / x n < 8 + 1 := by sorry
Source
For we have and , so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_43025 (x : ℕ → ℝ) (hx: ∀ n, 1 <= x n ∧ x n <= 2) : ∀ n, x n ^ 3 + 1 / x n < 8 + 1 := by sorry