lean_workbook_plus_10454
ProvedNote that for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10454 (x : ℝ) (hx : 0 < x) : Real.sqrt (x ^ 2 + 1) < x + 1 := by sorry
Source
Note that for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_10454 (x : ℝ) (hx : 0 < x) : Real.sqrt (x ^ 2 + 1) < x + 1 := by sorry