Prove2Me

lean_workbook_plus_48056

Proved

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

Let a,b,ca,b,c be reals . Prove that \n

0≤(1−a)(1−b)(1−a−b+ab)(1+a2)(1+b2)≤40\leq\frac{(1-a)(1-b)(1-a-b+ab)}{(1+a^2)(1+b^2)}\leq4
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48056 (a b c : ℝ) : 0 ≤ (1 - a) * (1 - b) * (1 - a - b + a * b) / ((1 + a ^ 2) * (1 + b ^ 2)) ∧ (1 - a) * (1 - b) * (1 - a - b + a * b) / ((1 + a ^ 2) * (1 + b ^ 2)) ≤ 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph