continuous_const_cpow

Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

English

For any z ≠ 0, the map s ↦ z^s is continuous as a function of s.

Русский

Для любого z ≠ 0 отображение s ↦ z^s непрерывно по s.

LaTeX

$$$$\\forall z\\in \\mathbb{C},\\ z\\neq 0\\;\\Rightarrow\\; \\text{Continuous}(s \\mapsto z^{s}). $$$$

Lean4

@[fun_prop]
theorem continuous_const_cpow (z : ℂ) [NeZero z] : Continuous fun s : ℂ ↦ z ^ s :=
  continuous_id.const_cpow (.inl <| NeZero.ne z)

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

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

Разделы

Аффилиация

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