cpow

Mathlib.Analysis.SpecialFunctions.Pow.Continuity

URI: https://scilib.ai/kg/mathlib#ContinuousAt.cpow

← MathLib Explorer

English

For a fixed a ≠ 0, the map x ↦ a^x is continuous at any b.

Русский

При фиксированном a ≠ 0 отображение x ↦ a^x непрерывно в любой точке b.

LaTeX

$$$$\\forall a \\in \\mathbb{C}, a \\neq 0,\\quad \\text{ContinuousAt}(\\lambda x. a^{x}, b).$$$$

Lean4

nonrec theorem cpow (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h0 : f a ∈ slitPlane) :
    ContinuousAt (fun x => f x ^ g x) a :=
  hf.cpow hg h0

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

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

Разделы

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

Аффилиация

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