continuous_coe — Mathlib

English

The natural projection (coe) from the restricted product to the full product is continuous.

Русский

Естественная проекция (coe) из ограниченного произведения в полное произведение непрерывна.

LaTeX

$$$\\operatorname{coe} : \\prod^{\\mathrm{r}} i, [R i, A i]_{\\mathcal F} \\to \\prod i, R_i$ is continuous.$$

Lean4

@[fun_prop]
theorem continuous_coe : Continuous ((↑) : Πʳ i, [R i, A i]_[𝓕] → Π i, R i) :=
  continuous_iSup_dom.mpr fun _ ↦ continuous_iSup_dom.mpr fun _ ↦ continuous_coinduced_dom.mpr continuous_induced_dom

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