ball — Mathlib

English

The ball around x with respect to V is the preimage of V under the map p ↦ (x,p).

Русский

Окружение вокруг x с отношением V определяется как множество {p : β | (x,p) ∈ V}.

LaTeX

$$$$\\mathrm{ball}(x,V) = (\\mathrm{Prod.mk}\\ x)^{-1}(V).$$$$

Lean4

/-- The ball around `(x : β)` with respect to `(V : Set (β × β))`. Intended to be
used for `V ∈ 𝓤 β`, but this is not needed for the definition. Recovers the
notions of metric space ball when `V = {p | dist p.1 p.2 < r }`. -/
def ball (x : β) (V : Set (β × β)) : Set β :=
  Prod.mk x ⁻¹' V

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