compContinuousMap — Mathlib

English

Given a Homotopy G: g0 ~ g1 between maps Y → Z and a map f: X → Y, then G comp f defines a Homotopy between g0 ∘ f and g1 ∘ f.

Русский

Пусть G: g0 ~ g1 — гомотопия между отображениями Y → Z, и пусть f: X → Y. Тогда G ∘ f задаёт гомотопию между g0 ∘ f и g1 ∘ f.

LaTeX

$$$$ (G \circ f) : \mathrm{Homotopy}(g_0 \circ f, g_1 \circ f) $$$$

Lean4

/-- Composition of a `Homotopy g₀ g₁` and `f : C(X, Y)` as a homotopy between `g₀.comp f` and
`g₁.comp f`. -/
@[simps!]
def compContinuousMap {g₀ g₁ : C(Y, Z)} (G : Homotopy g₀ g₁) (f : C(X, Y)) : Homotopy (g₀.comp f) (g₁.comp f) :=
  G.comp (.refl f)

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