Interval_Defined_by_Absolute_Value

Proved

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

absolute-value-functionproofwikireal-intervals

Let $\xi, \delta \in \R$ be real numbers. Let $\delta > 0$ . Then

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Interval_Defined_by_Absolute_Value (xi delta : ℝ) (hd : 0 < delta) (x : ℝ) : |x - xi| < delta ↔ xi - delta < x ∧ x < xi + delta := by sorry

Source

https://proofwiki.org/wiki/Interval_Defined_by_Absolute_Value

View graph