English
If a family F of group endomorphisms from G to M is equicontinuous at the identity, then it is equicontinuous on all of G.
Русский
Если семейство эндоморфизмов группы G в M эквиконтинуально в точке единицы, то оно экконтинуально на всём G.
LaTeX
$$EquicontinuousAt((↑) ∘ F) (1_G) ⇒ Equicontinuous((↑) ∘ F)$$
Lean4
@[to_additive]
theorem equicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [TopologicalSpace G] [UniformSpace M] [Group G]
[Group M] [IsTopologicalGroup G] [IsUniformGroup M] [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom)
(hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) : Equicontinuous ((↑) ∘ F) :=
by
rw [equicontinuous_iff_continuous]
rw [equicontinuousAt_iff_continuousAt] at hf
let φ : G →* (ι →ᵤ M) :=
{ toFun := swap ((↑) ∘ F)
map_one' := by dsimp [UniformFun]; ext; exact map_one _
map_mul' := fun a b => by dsimp [UniformFun]; ext; exact map_mul _ _ _ }
exact continuous_of_continuousAt_one φ hf
