analyticOnNhd_id — Mathlib

English

The identity map id is analytic on nhds; i.e., AnalyticOnNhd 𝕜 id s holds for any s that contains a neighborhood of points in E.

Русский

Тождественное отображение id аналитично на окрестностях; то есть AnalyticOnNhd 𝕜 id s выполняется для любого s, содержащего окрестности точек в E.

LaTeX

$$$AnalyticOnNhd 𝕜 (id : E \\to E) s$$$

Lean4

/-- `id` is entire -/
theorem analyticOnNhd_id : AnalyticOnNhd 𝕜 (fun x : E ↦ x) s := fun _ _ ↦ analyticAt_id

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