closedBall — Mathlib

English

For any p, x, r, and y, y belongs to ball p x r exactly when p(y − x) < r.

Русский

Членство y в шаре по p вокруг x радиуса r эквивалентно условию p(y − x) < r.

LaTeX

$$$y \\in \\mathrm{ball}_p(x,r) \\iff p(y - x) < r$$$

Lean4

/-- The closed ball of radius `r` at `x` with respect to seminorm `p` is the set of elements `y`
with `p (y - x) ≤ r`. -/
def closedBall (x : E) (r : ℝ) :=
  {y : E | p (y - x) ≤ r}

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