Theorems · Theorem · general topology

Metric.mk_uniformity_basis_le

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

Given f : β → ℝ, if f sends {i | p i} to a set of positive numbers accumulating to zero, then closed neighborhoods of the diagonal of sizes {f i | p i} form a basis of 𝓤 α. Currently we have only one specific basis uniformity_basis_dist_le based on this constructor. More can be easily added if needed in the future.

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

4 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace