lean_workbook_plus_66330

Proved

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

Show that, for all $\alpha_i$ , the equations $\beta_1 + \beta_3 = \alpha_1$ , $\beta_1 + \beta_2 = \alpha_2$ , $\beta_2 + \beta_3 = \alpha_3$ can be satisfied.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66330 (α₁ α₂ α₃ : ℝ) : ∃ β₁ β₂ β₃ : ℝ, β₁ + β₃ = α₁ ∧ β₁ + β₂ = α₂ ∧ β₂ + β₃ = α₃   :=  by sorry

Source

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

View graph