lean_workbook_plus_25115
Provedprove
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25115 : ∀ x : ℝ, x ≠ 0 → 1 + 1 / (2 * x ^ 2) ≥ Real.sqrt ((1 + x ^ 2) / x ^ 2) := by sorry
Source
prove
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_25115 : ∀ x : ℝ, x ≠ 0 → 1 + 1 / (2 * x ^ 2) ≥ Real.sqrt ((1 + x ^ 2) / x ^ 2) := by sorry