Algebra-related equicontinuity criterions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
equicontinuous_of_equicontinuous_at_one
{ι : Type u_1}
{G : Type u_2}
{M : Type u_3}
{hom : Type u_4}
[topological_space G]
[uniform_space M]
[group G]
[group M]
[topological_group G]
[uniform_group M]
[monoid_hom_class hom G M]
(F : ι → hom)
(hf : equicontinuous_at (coe_fn ∘ F) 1) :
equicontinuous (coe_fn ∘ F)
theorem
equicontinuous_of_equicontinuous_at_zero
{ι : Type u_1}
{G : Type u_2}
{M : Type u_3}
{hom : Type u_4}
[topological_space G]
[uniform_space M]
[add_group G]
[add_group M]
[topological_add_group G]
[uniform_add_group M]
[add_monoid_hom_class hom G M]
(F : ι → hom)
(hf : equicontinuous_at (coe_fn ∘ F) 0) :
equicontinuous (coe_fn ∘ F)
theorem
uniform_equicontinuous_of_equicontinuous_at_zero
{ι : Type u_1}
{G : Type u_2}
{M : Type u_3}
{hom : Type u_4}
[uniform_space G]
[uniform_space M]
[add_group G]
[add_group M]
[uniform_add_group G]
[uniform_add_group M]
[add_monoid_hom_class hom G M]
(F : ι → hom)
(hf : equicontinuous_at (coe_fn ∘ F) 0) :
theorem
uniform_equicontinuous_of_equicontinuous_at_one
{ι : Type u_1}
{G : Type u_2}
{M : Type u_3}
{hom : Type u_4}
[uniform_space G]
[uniform_space M]
[group G]
[group M]
[uniform_group G]
[uniform_group M]
[monoid_hom_class hom G M]
(F : ι → hom)
(hf : equicontinuous_at (coe_fn ∘ F) 1) :