lean_workbook_plus_18955

Proved

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

Let $a, b$ be real numbers that $|a|<1$ and $|b|<1$ . Prove that $\left|\frac{a+b}{1+ab}\right|<1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18955 (a b : ℝ) (ha : abs a < 1) (hb : abs b < 1) : abs (a + b) / (1 + a * b) < 1   :=  by sorry

Source