continuous_const_rpow

Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

← MathLib Explorer

English

For any base a ≠ 0, the map x ↦ a^x is continuous on ℝ.

Русский

Для основания a ≠ 0 отображение x ↦ a^x непрерывно на ℝ.

LaTeX

$$$$\forall a\neq 0\Rightarrow \text{Continuous}(x \mapsto a^x).$$$$

Lean4

@[fun_prop]
theorem continuous_const_rpow {a : ℝ} (h : a ≠ 0) : Continuous (fun x : ℝ ↦ a ^ x) :=
  continuous_iff_continuousAt.mpr fun _ ↦ continuousAt_const_rpow h

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

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

Разделы

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

Аффилиация

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