lean_workbook_plus_3220
ProvedProve that if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3220 (a : ℝ) (h : 0 < a ∧ a < 2) : a < Real.sqrt (2 * a) ∧ Real.sqrt (2 * a) < 2 := by sorry
Source
Prove that if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3220 (a : ℝ) (h : 0 < a ∧ a < 2) : a < Real.sqrt (2 * a) ∧ Real.sqrt (2 * a) < 2 := by sorry