Theorems · Theorem · general topology

Metric.mk_uniformity_basis

∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ},
  (∀ (i : β), p i → 0 < f i) →
    (∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) → (uniformity α).HasBasis p fun i => {p | dist p.1 p.2 < f i}

Given f : β → ℝ, if f sends {i | p i} to a set of positive numbers accumulating to zero, then f i-neighborhoods of the diagonal form a basis of 𝓤 α. For specific bases see uniformity_basis_dist, uniformity_basis_dist_inv_nat_succ, and uniformity_basis_dist_inv_nat_pos.

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

7 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace