continuous_rpow_const

Mathlib.Analysis.SpecialFunctions.Pow.Continuity

URI: https://scilib.ai/kg/mathlib#Real.continuous_rpow_const

← MathLib Explorer

English

For any fixed q ≥ 0, the function x ↦ x^q is globally continuous on ℝ.

Русский

Для любого фиксированного q ≥ 0 функция x ↦ x^q непрерывна на всей ℝ.

LaTeX

$$$$\forall q\ge 0,\ \text{Continuous}(x \mapsto x^q)$$$$

Lean4

@[fun_prop]
theorem continuous_rpow_const {q : ℝ} (h : 0 ≤ q) : Continuous (fun x : ℝ => x ^ q) :=
  continuous_iff_continuousAt.mpr fun x ↦ continuousAt_rpow_const x q (.inr h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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