Integer powers in topological groups

Continuity results for integer powers and integer scalar multiplication in topological groups.

theorem continuous_zpow {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (z : ℤ) : Continuous fun (a : G) => a ^ z

theorem continuous_zsmul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (z : ℤ) : Continuous fun (a : G) => z • a

instance AddGroup.continuousConstSMul_int {A : Type u_3} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] : ContinuousConstSMul ℤ A

instance AddGroup.continuousSMul_int {A : Type u_3} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] : ContinuousSMul ℤ A

theorem Continuous.zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous (f ^ z)

theorem Continuous.fun_zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun (i : α) => f i ^ z

Eta-expanded form of Continuous.zpow

theorem Continuous.zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous (z • f)

theorem Continuous.fun_zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun (i : α) => z • f i

theorem continuousOn_zpow {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (z : ℤ) : ContinuousOn (fun (x : G) => x ^ z) s

theorem continuousOn_zsmul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (z : ℤ) : ContinuousOn (fun (x : G) => z • x) s

theorem continuousAt_zpow {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) (z : ℤ) : ContinuousAt (fun (x : G) => x ^ z) x

theorem continuousAt_zsmul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) (z : ℤ) : ContinuousAt (fun (x : G) => z • x) x

theorem Filter.Tendsto.zpow {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {α : Type u_3} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (nhds x)) (z : ℤ) : Tendsto (fun (x : α) => f x ^ z) l (nhds (x ^ z))

theorem Filter.Tendsto.zsmul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (nhds x)) (z : ℤ) : Tendsto (fun (x : α) => z • f x) l (nhds (z • x))

theorem ContinuousWithinAt.zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (f ^ z) s x

theorem ContinuousWithinAt.fun_zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (fun (i : α) => f i ^ z) s x

Eta-expanded form of ContinuousWithinAt.zpow

theorem ContinuousWithinAt.zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (z • f) s x

theorem ContinuousWithinAt.fun_zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (fun (i : α) => z • f i) s x

theorem ContinuousAt.zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (f ^ z) x

theorem ContinuousAt.fun_zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (fun (i : α) => f i ^ z) x

Eta-expanded form of ContinuousAt.zpow

theorem ContinuousAt.fun_zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (fun (i : α) => z • f i) x

theorem ContinuousAt.zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (z • f) x

theorem ContinuousOn.zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (f ^ z) s

theorem ContinuousOn.fun_zpow {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun (i : α) => f i ^ z) s

Eta-expanded form of ContinuousOn.zpow

theorem ContinuousOn.fun_zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun (i : α) => z • f i) s

theorem ContinuousOn.zsmul {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (z • f) s