comp — Mathlib

English

If g ∈ C(Y,R)₀ and f ∈ C(X,Y)₀, then the composition g ∘ f ∈ C(X,R)₀; i.e., composing two basepoint-preserving maps preserves the zero mapping.

Русский

Если g ∈ C(Y,R)₀ и f ∈ C(X,Y)₀, то составная карта g ∘ f ∈ C(X,R)₀; то есть композиция двух нулеподдерживающих отображений сохраняет ноль.

LaTeX

$$$(g\\circ f) \\in C(X,R)_0$ whenever $g\\in C(Y,R)_0$ and $f\\in C(X,Y)_0$$$

Lean4

/-- Composition of continuous maps which map zero to zero. -/
def comp (g : C(Y, R)₀) (f : C(X, Y)₀) : C(X, R)₀
    where
  toContinuousMap := (g : C(Y, R)).comp (f : C(X, Y))
  map_zero' := show g (f 0) = 0 from map_zero f ▸ map_zero g

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