lean_workbook_plus_35440
ProvedProve that for , .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35440 (u : ℝ) (h : u > 0) : u + (1 / u) ≥ 2 := by sorry
Source
Prove that for , .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35440 (u : ℝ) (h : u > 0) : u + (1 / u) ≥ 2 := by sorry