Theorems · Theorem · general topology

UniformOnFun.iInf_eq

∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ι → UniformSpace γ},
  UniformOnFun.uniformSpace α γ 𝔖 = ⨅ i, UniformOnFun.uniformSpace α γ 𝔖

If u is a family of uniform structures on γ, then 𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

1 results in Mathlib

Foundations

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