isSt_iff_abs_sub_lt_delta — Mathlib

English

IsSt x r iff for all δ > 0, |x − ↑r| < δ.

Русский

IsSt x r эквивалентно тому, что для всех δ > 0 выполняется |x − ↑r| < δ.

LaTeX

$$$\mathrm{IsSt}(x,r) \iff \forall \delta \in \mathbb{R}, \; \delta > 0 \Rightarrow |x - \uparrow r| < \delta$$$

Lean4

theorem isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} : IsSt x r ↔ ∀ δ : ℝ, 0 < δ → |x - ↑r| < δ := by
  simp only [abs_sub_lt_iff, sub_lt_iff_lt_add, IsSt, and_comm, add_comm]

Похожие утверждения