lean_workbook_plus_56771

Proved

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

Problema 6.\nSi $a_1, a_2, a_3 \geq 0$ y $(1 + a_1)(1 + a_2)(1 + a_3) = 8.$ \nMostrar que:\n $a_1.a_2.a_3 \leq 1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56771 (a₁ a₂ a₃ : ℝ) (h₁ : 0 ≤ a₁) (h₂ : 0 ≤ a₂) (h₃ : 0 ≤ a₃) (h : (1 + a₁) * (1 + a₂) * (1 + a₃) = 8) : a₁ * a₂ * a₃ ≤ 1   :=  by sorry

Source

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

View graph