lean_workbook_plus_23412

Proved

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

Let $n$ be any natural numbers and $x,y$ are real numbers with $0<x<y$ . Is it true that $\sqrt[n]{x}-\sqrt[n]{y}\leq \sqrt[n]{y-x}$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23412 (n : ℕ) (x y : ℝ) (hx : x > 0) (hy : y > x) : (x:ℝ) ^ (1 / n) - (y:ℝ) ^ (1 / n) ≤ (y - x:ℝ) ^ (1 / n)   :=  by sorry

Source