analyticAt_id — Mathlib

English

The identity map id: E → E is analytic at every point; in particular AnalyticAt 𝕜 id z holds for any z ∈ E.

Русский

Быть аналитичной сохраняется у тождественного отображения id: E → E во всех точках; то есть AnalyticAt 𝕜 id z справедливо для любого z ∈ E.

LaTeX

$$$AnalyticAt 𝕜 (id : E \\to E) z$$$

Lean4

@[fun_prop]
theorem analyticAt_id : AnalyticAt 𝕜 (id : E → E) z :=
  (ContinuousLinearMap.id 𝕜 E).analyticAt z

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