lean_workbook_plus_30908
ProvedThe inequality when .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30908 : ∀ z : ℝ, 1 ≤ z → 2 * z / (1 / z + z) ≥ 1 := by sorry
Source
The inequality when .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30908 : ∀ z : ℝ, 1 ≤ z → 2 * z / (1 / z + z) ≥ 1 := by sorry