lean_workbook_plus_17447

Proved

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

If $0 \le a, b, c, d \le 1$ then: \n\n $(1-a)(1-b)(1-c)(1-d)+ a+b+c+d \ge 1 \ \ ;$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17447 (a b c d : ℝ) (h1 : 0 ≤ a ∧ a ≤ 1) (h2 : 0 ≤ b ∧ b ≤ 1) (h3 : 0 ≤ c ∧ c ≤ 1) (h4 : 0 ≤ d ∧ d ≤ 1) : (1 - a) * (1 - b) * (1 - c) * (1 - d) + a + b + c + d ≥ 1   :=  by sorry

Source

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

View graph