Theorems · Theorem · general topology

uniformEquicontinuous_iInf_rng

∀ {ι : Type u_1} {κ : Type u_2} {α' : Type u_7} {β : Type u_8} [uβ : UniformSpace β] {u : κ → UniformSpace α'}
  {F : ι → β → α'}, UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace