comp_continuousMap — Mathlib

English

If f0 ~_S f1 Rel-homotopy and g: Y→Z is continuous, then g∘f0 ~_S g∘f1.

Русский

Если f0 гомотопно относительно f1 по S, и g: Y→Z непрерывно, то g∘f0 гомотопно относительно g∘f1 по S.

LaTeX

$$$ \\forall f_0,f_1:\\,C(X,Y),\\;HomotopicRel(f_0,f_1,S) \\to \\forall g:\\,C(Y,Z), (g\\circ f_0)\\;HomotopicRel\\; (g\\circ f_1) S$$$

Lean4

theorem comp_continuousMap ⦃f₀ f₁ : C(X, Y)⦄ (h : f₀.HomotopicRel f₁ S) (g : C(Y, Z)) :
    (g.comp f₀).HomotopicRel (g.comp f₁) S :=
  h.map (·.compContinuousMap g)

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