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} [TopologicalSpace G] [UniformSpace M] [AddGroup G] [AddGroup M] [TopologicalAddGroup G] [UniformAddGroup M] [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} [TopologicalSpace G] [UniformSpace M] [Group G] [Group M] [TopologicalGroup G] [UniformGroup M] [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} [UniformSpace G] [UniformSpace M] [AddGroup G] [AddGroup M] [UniformAddGroup G] [UniformAddGroup M] [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} [UniformSpace G] [UniformSpace M] [Group G] [Group M] [UniformGroup G] [UniformGroup M] [MonoidHomClass hom G M] (F : ιhom) (hf : EquicontinuousAt (FunLike.coe F) 1) :
UniformEquicontinuous (FunLike.coe F)