Theorems · Theorem · general topology

UniformOnFun.hasBasis_uniformity_of_covering_of_basis

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} {ι' : Type u_6} [Nonempty ι]
  {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)},
  (∀ (i : ι), t i ∈ 𝔖) →
    Directed (fun x1 x2 => x1 ⊆ x2) t →
      (∀ s ∈ 𝔖, ∃ i, s ⊆ t i) →
        (uniformity β).HasBasis p V →
          (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun i => p i.2) fun i => UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Let t i be a nonempty directed subfamily of 𝔖 such that every s ∈ 𝔖 is included in some t i. Let V bounded by p be a basis of entourages of β. Then UniformOnFun.gen 𝔖 (t i) (V j) bounded by p j is a basis of entourages of α →ᵤ[𝔖] β.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceNonempty