Theorems · Theorem · general topology

uniformEquicontinuousOn_iInf_dom

∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β' : Type u_9} [uα : UniformSpace α] {u : κ → UniformSpace β'}
  {F : ι → β' → α} {S : Set β'} {k : κ}, UniformEquicontinuousOn F S → UniformEquicontinuousOn F S

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpace