continuousOn_zpow

Mathlib.Topology.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#continuousOn_zpow

English

For any z ∈ ℤ, the map x ↦ x^z is continuous on any set s ⊆ G.

Русский

Для любого z ∈ ℤ отображение x ↦ x^z непрерывно на любом множества s ⊆ G.

LaTeX

$$$\forall z\in\mathbb{Z},\; \text{ContinuousOn}(x \mapsto x^{z}, s).$$$

Lean4

@[to_additive]
theorem continuousOn_zpow {s : Set G} (z : ℤ) : ContinuousOn (fun x => x ^ z) s :=
  (continuous_zpow z).continuousOn

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru