lean_workbook_plus_2123
ProvedIf , then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2123 (x : ℝ) (hx : 0 < x ∧ x < 1) : x^3 < 1 ∧ 1 < x^4 + 1 := by sorry
Source
If , then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2123 (x : ℝ) (hx : 0 < x ∧ x < 1) : x^3 < 1 ∧ 1 < x^4 + 1 := by sorry