continuous_apply — Mathlib

English

Each coordinate projection composition with the PiLp-to-β_i map is continuous: f ↦ f(i).

Русский

Пусть i-й проекцией является непрерывное отображение, композиция: f ↦ f(i).

LaTeX

$$$$\\text{continuous_apply}(i):\\; \\text{Continuous}(\\lambda f:\\PiLp(p,\\beta)\\mapsto f(i)).$$$$

Lean4

@[fun_prop, continuity]
protected theorem continuous_apply [∀ i, TopologicalSpace (β i)] (i : ι) : Continuous (fun f : PiLp p β ↦ f i) :=
  (continuous_apply i).comp (continuous_ofLp p β)

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