# Algebra-related equicontinuity criterions #

theorem equicontinuous_of_equicontinuousAt_zero {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [] [] [] [] [] [FunLike hom G M] [AddMonoidHomClass hom G M] (F : ιhom) (hf : EquicontinuousAt (DFunLike.coe F) 0) :
Equicontinuous (DFunLike.coe F)
theorem equicontinuous_of_equicontinuousAt_one {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [] [] [] [] [] [] [FunLike hom G M] [MonoidHomClass hom G M] (F : ιhom) (hf : EquicontinuousAt (DFunLike.coe F) 1) :
Equicontinuous (DFunLike.coe F)
theorem uniformEquicontinuous_of_equicontinuousAt_zero {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [] [] [] [] [] [] [FunLike hom G M] [AddMonoidHomClass hom G M] (F : ιhom) (hf : EquicontinuousAt (DFunLike.coe F) 0) :
UniformEquicontinuous (DFunLike.coe F)
theorem uniformEquicontinuous_of_equicontinuousAt_one {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [] [] [] [] [] [] [FunLike hom G M] [MonoidHomClass hom G M] (F : ιhom) (hf : EquicontinuousAt (DFunLike.coe F) 1) :
UniformEquicontinuous (DFunLike.coe F)