analyticOnNhd_log

Mathlib.Analysis.SpecialFunctions.Complex.Analytic

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

English

The real logarithm is analytic on a neighborhood of positive real numbers.

Русский

Реальная логарифм аналитичен в окрестности положительных вещественных чисел.

LaTeX

$$$\\text{analyticOnNhd}_\\mathbb{R}(\\operatorname{Real.log})(\\,\\mathbb{I}^+)\\,$$$

Lean4

theorem analyticOnNhd_log : AnalyticOnNhd ℝ Real.log (Set.Ioi 0) := fun _ hx ↦ analyticAt_log hx

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

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

Разделы

Аффилиация

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