no goals
α✝ : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 => x) l (𝓝 x)
h : Tendsto (fun n => u n / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)
simpa using h.mul A
no goals
α✝ : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 => x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun n => u n / x) l (𝓝 1)
simpa using h.div' A