Theorems · Theorem · general topology

UniformOnFun.isCountablyGenerated_uniformity

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) [(uniformity β).IsCountablyGenerated]
  {t : ℕ → Set α},
  (∀ (n : ℕ), t n ∈ 𝔖) → Monotone t → (∀ s ∈ 𝔖, ∃ n, s ⊆ t n) → (uniformity (UniformOnFun α β 𝔖)).IsCountablyGenerated

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceFilter.IsCountablyGenerated