Theorems · Theorem · general topology

UniformOnFun.hasBasis_nhds_zero_of_basis

∀ {α : Type u_1} {G : Type u_2} {ι : Type u_3} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G]
  (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {b : ι → Set G},
        (nhds 0).HasBasis p b →
          (nhds 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
            {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}

Defined in

Mathlib.Topology.Algebra.UniformConvergence

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupUniformSpaceIsUniformAddGroup