lean_workbook_plus_52299

Proved

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

Since two notes above, \n $\frac{|x-y|}{1+|x-y|}\le \frac{|2x+y|+|x+2y|}{1+|2x+y|+|x+2y|}$ \n $=\frac{|2x+y|}{1+|2x+y|+|x+2y|}+\frac{|x+2y|}{1+|2x+y|+|x+2y|}$ \n $\le \frac{|2x+y|}{1+|2x+y|}+\frac{|x+2y|}{1+|x+2y|}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52299  (x y : ℝ) :
  abs (x - y) / (1 + abs (x - y)) ≤ (abs (2 * x + y) + abs (x + 2 * y)) / (1 + abs (2 * x + y) + abs (x + 2 * y))   :=  by sorry

Source

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

View graph