lean_workbook_plus_30931

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that if $x>0$ , then $g(x)=x+\frac{1}{x}\geq 2$ with equality if and only if $x=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30931 (x : ℝ) (hx: x > 0) : x + 1/x ≥ 2 ∧ (x = 1 ↔ x + 1/x = 2)   :=  by sorry

Source