lean_workbook_plus_21336

Proved

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

To prove induction step observe that for positive $x,y$ $\frac{1}{1+x}+\frac{1}{1+y}\leq \frac{1}{1+xy}+1,$ $\frac{2+x+y}{(1+x)(1+y)}\leq \frac{1}{1+xy}+1,$ $\frac{1-xy}{(1+x)(1+y)}\leq \frac{1}{1+xy},$ and $1-x^2y^2\leq 1\leq (1+x)(1+y)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21336  (x y : ℝ)
  (h₀ : 0 < x ∧ 0 < y) :
  1 / (1 + x) + 1 / (1 + y) ≤ 1 / (1 + x * y) + 1   :=  by sorry

Source

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

View graph