lean_workbook_plus_8890

Proved

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

Let $a+b-c=x$ \nb+c-a=y \nc+a-b=z \nSo we get $(x+y)/2=b$ \n $(z+y)/2= c$ \n $(x+z)/2=a$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph