continuous_precomp — Mathlib

English

For a fixed f ∈ C(X, Y), the map g ↦ g ∘ f from C(Y, Z) to C(X, Z) is continuous.

Русский

Для фиксированного отображения f: X → Y отображение g ↦ g ∘ f с пространства C(Y, Z) в C(X, Z) непрерывно.

LaTeX

$$$\\text{Continuous}(\\, g \\mapsto g \\circ f\\,)$$$

Lean4

/-- `C(·, Z)` is a functor. -/
@[continuity, fun_prop]
theorem continuous_precomp (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
  continuous_compactOpen.2 fun K hK U hU ↦ by simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU

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