lean_workbook_plus_29209

Proved

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

Now from given condition we have $f(x)>\frac {1}{\sqrt x}$ for all $x\mathbb{R}^+$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29209 (x : ℝ) (f : ℝ → ℝ) (hf: f x > 1 / Real.sqrt x): ∃ x, f x > 1 / Real.sqrt x   :=  by sorry

Source