Theorems · Theorem · general topology

Metric.mk_uniformity_basis_of_tendsto

∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ} {l : Filter β} [l.NeBot],
  (∀ (i : β), p i → 0 < f i) →
    (∀ᶠ (i : β) in l, p i) → Filter.Tendsto f l (nhds 0) → (uniformity α).HasBasis p fun i => {x | dist x.1 x.2 < f i}

If f is a positive radius tending to zero, then the sets of pairs with distance less than f i form a basis of the uniformity.

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

1 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceFilter.NeBot