lean_workbook_plus_75108

Proved

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

Let $f(x) = x - \frac{1}{x}$ , prove that $f$ is an increasing function for $x > 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75108 (x y : ℝ) (h₁ : x > 0 ∧ y > 0) (h₂ : x < y) : x - 1/x < y - 1/y   :=  by sorry

Source