homotopic — Mathlib

English

If two maps are homotopic relative to a set S, then they are homotopic (without the relative condition).

Русский

Если две отображения гомотопны относительно множества S, то они гомотопны без условия относительности.

LaTeX

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

Lean4

/-- If two maps are homotopic relative to a set, then they are homotopic. -/
protected theorem homotopic {f₀ f₁ : C(X, Y)} (h : HomotopicRel f₀ f₁ S) : Homotopic f₀ f₁ :=
  h.map fun F ↦ F.1

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