analyticOn_toLp — Mathlib

English

The function toLp(p) is analytic on any set; equivalently, the product continuous linear equivalence furnishes an analytic map.

Русский

Функция toLp(p) аналитична на любом множестве; эквивалентно, что произведение непрерывно-линейных отображений даёт аналитическую карту.

LaTeX

$$$\\text{AnalyticOn}_{\\mathbb{k}}(\\mathrm{toLp}(p))\\; s.$$$

Lean4

theorem analyticOn_toLp (s : Set (E × F)) : AnalyticOn 𝕜 (toLp p) s :=
  (prodContinuousLinearEquiv p 𝕜 E F).symm.analyticOn s

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