lean_workbook_plus_1768
ProvedBut from Bernoulli we have that : \n\n \n\n \n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1768 (x y z : ℝ) : x^2 ≥ 2*x-1 ∧ y^4 ≥ 4*y-3 ∧ z^8 ≥ 8*z-7 := by sorry
Source
But from Bernoulli we have that : \n\n \n\n \n\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1768 (x y z : ℝ) : x^2 ≥ 2*x-1 ∧ y^4 ≥ 4*y-3 ∧ z^8 ≥ 8*z-7 := by sorry