Theorems · Theorem · general topology

UniformOnFun.hasBasis_uniformity_of_basis

∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {s : ι → Set (β × β)},
        (uniformity β).HasBasis p s →
          (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
            UniformOnFun.gen 𝔖 Si.1 (s Si.2)

If 𝔖 : Set (Set α) is nonempty and directed and 𝓑 is a filter basis of 𝓤 β, then the uniformity of α →ᵤ[𝔖] β admits the family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓑 as a filter basis.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpace