∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] [CompactSpace X],
  Equicontinuous F → (Topology.IsInducing (⇑UniformFun.ofFun ∘ F) ↔ Topology.IsInducing F)