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]
:
instance
AddGroup.continuousSMul_int
{A : Type u_3}
[AddGroup A]
[TopologicalSpace A]
[IsTopologicalAddGroup 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 : ℤ)
:
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 : ℤ)
:
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