continuous_postcomp — Mathlib

English

For any g ∈ C(Y,Z), the postcomposition with g, seen as a map from C(X,Y) to C(X,Z), is continuous.

Русский

Для любого g ∈ C(Y,Z) композиция справа с g, как отображение C(X,Y) → C(X,Z), непрерывна.

LaTeX

$$$ \\text{continuous_postcomp}(g) : \\text{Continuous} (\\text{ContinuousMap.comp } g : C(X, Y) \\to C(X, Z)) $$$

Lean4

/-- `C(X, ·)` is a functor. -/
theorem continuous_postcomp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) :=
  continuous_compactOpen.2 fun _K hK _U hU ↦ isOpen_setOf_mapsTo hK (hU.preimage g.2)

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