lean_workbook_plus_29662

Proved

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

Let $1\ge x\ge y\ge z\ge 0$ ,and $a=\sqrt{x-y} ,b=\sqrt{y-z}, c=\sqrt{x-z}$ , so $a^2+b^2=c^2 ,$ and $0\le c \le1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29662 (x y z a b c: ℝ) (h₁ : 1 ≥ x ∧ x ≥ y ∧ y ≥ z ∧ z ≥ 0)(h₂ : a = Real.sqrt (x - y) ∧ b = Real.sqrt (y - z) ∧ c = Real.sqrt (x - z))(h₃ : a^2 + b^2 = c^2): 0 ≤ c ∧ c ≤ 1   :=  by sorry

Source

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

View graph