lean_workbook_plus_82301
Disprovedproofwiki
If then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82301 (x : ℝ) (h : 0 < x ∧ x < 1) : Real.sqrt (1 + x^2) > Real.sqrt (1 + x) := by sorry
Source
If then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_82301 (x : ℝ) (h : 0 < x ∧ x < 1) : Real.sqrt (1 + x^2) > Real.sqrt (1 + x) := by sorry