Theorems · Theorem · general topology

UniformOnFun.hasAntitoneBasis_uniformity

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} [inst_1 : Preorder ι]
  [IsDirectedOrder ι] {t : ι → Set α} {V : ι → Set (β × β)},
  (∀ (n : ι), t n ∈ 𝔖) →
    Monotone t →
      (∀ s ∈ 𝔖, ∃ n, s ⊆ t n) →
        (uniformity β).HasAntitoneBasis V →
          (uniformity (UniformOnFun α β 𝔖)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)

If t n is a monotone sequence of sets in 𝔖 such that each s ∈ 𝔖 is included in some t n and V n is an antitone basis of entourages of β, then UniformOnFun.gen 𝔖 (t n) (V n) is an antitone basis of entourages of α →ᵤ[𝔖] β.

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpacePreorderIsDirectedOrder