isOpenMap_apply — Mathlib

English

For each index i, the projection sending a function f to its i-th coordinate f(i) is an open map from PiLp p β to β_i.

Русский

Для каждого индекса i отображение проекции, отправляющее f в его i-ю координату f(i), является открытым отображением из PiLp p β в β_i.

LaTeX

$$IsOpenMap (fun f : PiLp p β ↦ f i)$$

Lean4

theorem isOpenMap_apply [∀ i, TopologicalSpace (β i)] (i : ι) : IsOpenMap (fun f : PiLp p β ↦ f i) :=
  (isOpenMap_eval i).comp (homeomorph p β).symm.isOpenMap

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