analyticAt_snd

Mathlib.Analysis.Analytic.Linear

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

English

The projection onto the second coordinate, snd: E × F → F, is analytic at every point.

Русский

Проекция на вторую координату, snd: E × F → F, аналитична во всех точках.

LaTeX

$$$AnalyticAt 𝕜 (\\lambda p : E \\times F. p.2) p$$$

Lean4

/-- `snd` is analytic -/
theorem analyticAt_snd : AnalyticAt 𝕜 (fun p : E × F ↦ p.snd) p :=
  (ContinuousLinearMap.snd 𝕜 E F).analyticAt p

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

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

Разделы

Аффилиация

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