continuous_postcomp — Mathlib

English

If g : X → Y is continuous, then the map which sends f ∈ ∏_{i} X to g ∘ f ∈ ∏_{i} Y is continuous.

Русский

Если g: X → Y непрерывно, то отображение f ↦ (i ↦ g(f(i))) из произведения X в произведение Y непрерывно.

LaTeX

$$$\forall \; g: X \to Y,\; \text{Continuous}(g) \Rightarrow \; \text{Continuous}(\lambda f. (i \mapsto g(f(i))))$$$

Lean4

theorem continuous_postcomp [TopologicalSpace Y] {g : X → Y} (hg : Continuous g) :
    Continuous (g ∘ · : (ι → X) → (ι → Y)) :=
  Pi.continuous_postcomp' fun _ ↦ hg

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