English
In uniform spaces, if a family F: ι → hom is equicontinuous at 1, then it is uniformly equicontinuous.
Русский
В равномерных пространствах, если семейство F: ι → гомоморфизм эквиконтинуально в точке 1, то оно равно uniformly эквиконтинуально.
LaTeX
$$UniformEquicontinuous((↑) ∘ F) from EquicontinuousAt((↑) ∘ F)(1_G)$$
Lean4
@[to_additive]
theorem uniformEquicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [UniformSpace G] [UniformSpace M] [Group G]
[Group M] [IsUniformGroup G] [IsUniformGroup M] [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom)
(hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) : UniformEquicontinuous ((↑) ∘ F) :=
by
rw [uniformEquicontinuous_iff_uniformContinuous]
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 uniformContinuous_of_continuousAt_one φ hf
