lean_workbook_plus_75953

Proved

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

Given three real numbers $p$ , $q$ , and $r$ where $0<p,q,r<1$ . Show that $pq+qr+rp-2pqr<1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75953 (p q r : ℝ) (hp : 0 < p ∧ p < 1) (hq : 0 < q ∧ q < 1) (hr : 0 < r ∧ r < 1) : p*q + q*r + r*p - 2*p*q*r < 1   :=  by sorry

Source

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

View graph