Theorems · Theorem · general topology

uniformContinuous_pi

∀ {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] {β : Type u_4} [inst : UniformSpace β]
  {f : β → (i : ι) → α i}, UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i

Defined in

Mathlib.Topology.UniformSpace.Pi

Cited by

12 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace