Prove2Me

lean_workbook_plus_72215

Proved

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

Find the range of f(x,y)f(x,y) , where f(x,y)=x+y1+xyf(x,y)=\frac{x+y}{1+xy} and −1<x<1−1<y<1\begin{array}{c}-1<x<1\\-1<y<1\end{array}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72215 (f : ℝ × ℝ → ℝ) (x y : ℝ) (fxy: f (x,y) = (x + y) / (1 + x*y)) : -1 < x ∧ x < 1 ∧ -1 < y ∧ y < 1 → -1 < f (x,y) ∧ f (x,y) < 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph