closedBall — Mathlib

English

Membership in closedBall is equivalent to a componentwise inequality: y ∈ closedBall(x,ε) iff edist(y,x) ≤ ε.

Русский

Принадлежность y к closedBall(x,ε) эквивалентна неравенству edist(y,x) ≤ ε.

LaTeX

$$$ y \in \operatorname{closedBall}(x,\varepsilon) \iff \operatorname{edist}(y,x) \le \varepsilon. $$$

Lean4

/-- `EMetric.closedBall x ε` is the set of all points `y` with `edist y x ≤ ε` -/
def closedBall (x : α) (ε : ℝ≥0∞) :=
  {y | edist y x ≤ ε}

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