mathlib3 documentation

topology.algebra.equicontinuity

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) :
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) :