# Documentation

Mathlib.Topology.Algebra.Equicontinuity

# Algebra-related equicontinuity criterions #

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