analyticAt_fst

Mathlib.Analysis.Analytic.Linear

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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