lean_workbook_plus_82579

Proved

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

Let $a+b = z, b+c = x, c+a = y=>a=\frac{y+z-x}{2},b=\frac{z+x-y}{2},c=\frac{x+y-z}{2}$ .where $x,y,z>0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82579 (x y z a b c : ℝ) : x > 0 ∧ y > 0 ∧ z > 0 ∧ a + b = z ∧ b + c = x ∧ c + a = y → a = (y + z - x) / 2 ∧ b = (z + x - y) / 2 ∧ c = (x + y - z) / 2   :=  by sorry

Source

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

View graph