Theorems · Definition · general topology

UniformSpace.ball

{β : Type ub} → β → Set (β × β) → Set β

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 }.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

113 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 10 definitions · uses no axioms