continuous_restrict — Mathlib

English

The restriction map from the product ∏_{i} A_i to the restricted product ∏_{i∈S} A_i is continuous for any subset S ⊆ I.

Русский

Ограничивающее отображение от произведения к ограниченному произведению по S непрерывно.

LaTeX

$$$\text{Continuous}((\cdot)|_S): \prod_{i} A_i \to \prod_{i\in S} A_i$$$

Lean4

@[continuity, fun_prop]
theorem continuous_restrict (S : Set ι) : Continuous (S.restrict : (∀ i : ι, A i) → (∀ i : S, A i)) :=
  Pi.continuous_precomp' ((↑) : S → ι)

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