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]
[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}
[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
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)
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)