lean_workbook_plus_19133

Proved

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

Let $x,y$ be positive real numbers such that $x+2y=2$ . Prove that

\left(x+\dfrac{1}{y}\right)\left(y+\dfrac{1}{x}\right){\geq}\dfrac{9}{2}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19133 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (hxy : x + 2 * y = 2) : (x + 1 / y) * (y + 1 / x) ≥ 9 / 2   :=  by sorry

Source