continuous_comp_left — Mathlib

English

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

Русский

Зафиксируем f ∈ C(X,Y)₀. Тогда отображение g ↦ g ∘ f непрерывно от C(Y,Z)₀ в C(X,Z)₀.

LaTeX

$$$\\text{continuous\_comp\_left } f: C(Y,Z)_0 \\to C(X,Z)_0$$$

Lean4

@[fun_prop]
theorem continuous_comp_left {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [Zero X]
    [Zero Y] [Zero Z] (f : C(X, Y)₀) : Continuous fun g : C(Y, Z)₀ ↦ g.comp f :=
  by
  rw [continuous_induced_rng]
  change Continuous fun g : C(Y, Z)₀ ↦ (g : C(Y, Z)).comp (f : C(X, Y))
  fun_prop

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