lean_workbook_plus_49807

Open

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

Prove that for any finite set of non-negative reals $A$ , $1+\sum_{x\in A} x\le \prod_{x\in A}(1+x)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49807 (A : Finset ℝ) (hA : ∀ x ∈ A, 0 ≤ x) :
  1 + ∑ x in A, x ≤ ∏ x in A, (1 + x)   :=  by sorry

Source