lean_workbook_plus_42749

Proved

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

prove that for all $(a,b) \in \mathbb{R}^2$ : \n $(a^{2}+1)(b^{2}+1)\ge a(b^{2}+1)+b(a^{2}+1)$ \n $\Leftrightarrow \frac{a}{a^2+1}+\frac{b}{b^2+1} \le 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42749 (a b : ℝ) : (a^2 + 1) * (b^2 + 1) ≥ a * (b^2 + 1) + b * (a^2 + 1) ↔ a / (a^2 + 1) + b / (b^2 + 1) ≤ 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph