continuousOn_pow

Mathlib.Topology.Algebra.Monoid

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

English

For every n, the map x ↦ x^n is continuous on any subset s of M.

Русский

Для каждого n отображение x ↦ x^n непрерывно на любом подмножестве s моноида M.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\text{ContinuousOn}(x \\mapsto x^n, s)$$$

Lean4

@[to_additive]
theorem continuousOn_pow {s : Set M} (n : ℕ) : ContinuousOn (fun (x : M) => x ^ n) s :=
  (continuous_pow n).continuousOn

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

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

Разделы

Аффилиация

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