Prove2Me

Lean-Workbook Syntax 49807: A product bounds one plus the sum

Proved
WorkbookSyntax.plus_49807

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For a finite set AA of nonnegative real numbers, 1+∑x∈Ax≤∏x∈A(1+x)1+\sum_{x\in A}x\le\prod_{x\in A}(1+x).

Source: Lean-Workbook row lean_workbook_plus_49807 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic
Formal statement
theorem WorkbookSyntax.plus_49807 (A : Finset ℝ) (hA : ∀ x ∈ A, 0 ≤ x) :
  1 + ∑ x ∈ A, x ≤ ∏ x ∈ A, (1 + x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_49807; immutable original Prove2Me node 2ae07208-cbb5-4283-a3fa-5b88a333b6d2

View graph