Algebra-related equicontinuity criterions

theorem equicontinuous_of_equicontinuousAt_one {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [TopologicalSpace G] [UniformSpace M] [Group G] [Group M] [TopologicalGroup G] [UniformGroup M] [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt (DFunLike.coe ∘ F) 1) : Equicontinuous (DFunLike.coe ∘ F)

theorem equicontinuous_of_equicontinuousAt_zero {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [TopologicalSpace G] [UniformSpace M] [AddGroup G] [AddGroup M] [TopologicalAddGroup G] [UniformAddGroup M] [FunLike hom G M] [AddMonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt (DFunLike.coe ∘ F) 0) : Equicontinuous (DFunLike.coe ∘ F)

theorem uniformEquicontinuous_of_equicontinuousAt_one {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [UniformSpace G] [UniformSpace M] [Group G] [Group M] [UniformGroup G] [UniformGroup M] [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt (DFunLike.coe ∘ F) 1) : UniformEquicontinuous (DFunLike.coe ∘ F)

theorem uniformEquicontinuous_of_equicontinuousAt_zero {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [UniformSpace G] [UniformSpace M] [AddGroup G] [AddGroup M] [UniformAddGroup G] [UniformAddGroup M] [FunLike hom G M] [AddMonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt (DFunLike.coe ∘ F) 0) : UniformEquicontinuous (DFunLike.coe ∘ F)