analyticWithinAt_id — Mathlib

English

The identity map id: E → E is analytic within any set s at any point z ∈ E; i.e., AnalyticWithinAt 𝕜 id s z holds.

Русский

Тождественное отображение id: E → E аналитично внутри любого множества s в точке z ∈ E; то есть AnalyticWithinAt 𝕜 id s z справедливо.

LaTeX

$$$AnalyticWithinAt 𝕜 (id : E \\to E) s z$$$

Lean4

theorem analyticWithinAt_id : AnalyticWithinAt 𝕜 (id : E → E) s z :=
  analyticAt_id.analyticWithinAt

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