lean_workbook_plus_16752

Proved

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

If $\sqrt {x^2 + y^2 + z^2} < \varepsilon$ then $|x| < \varepsilon$ , $|y| < \varepsilon$ and $|z| < \varepsilon$ . Therefore ....

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16752 (x y z ε : ℝ) (h : Real.sqrt (x ^ 2 + y ^ 2 + z ^ 2) < ε) :
  |x| < ε ∧ |y| < ε ∧ |z| < ε   :=  by sorry

Source