lean_workbook_plus_66413

Proved

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

Let be three real numbers $a,b,c\in [0,1]$ satisfying the condition $ab+bc+ca=1.$ Prove that: $a+b+c+abc \leq 2$ and determine the cases in which equality is attained.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66413 (a b c : ℝ) (h : a ∈ Set.Icc 0 1 ∧ b ∈ Set.Icc 0 1 ∧ c ∈ Set.Icc 0 1) (h2: a * b + b * c + c * a = 1) : a + b + c + a * b * c ≤ 2   :=  by sorry

Source

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

View graph