Theorems · Theorem · general topology

EMetric.mk_uniformity_basis_le

∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal},
  (∀ (x : β), p x → 0 < f x) →
    (∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}

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

Defined in

Mathlib.Topology.EMetricSpace.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace