hcomp — Mathlib

English

A deprecated variant of composing homotopies: if f0 ~ f1 and g0 ~ g1, then g0 ∘ f0 ~ g1 ∘ f1.

Русский

Устаревшая форма композиции гомотопий: если f0 ~ f1 и g0 ~ g1, то g0 ∘ f0 ~ g1 ∘ f1.

LaTeX

$$$$ f_0 \sim f_1 \Rightarrow g_0 \sim g_1 \Rightarrow (g_0 \circ f_0) \sim (g_1 \circ f_1) $$$$

Lean4

@[deprecated comp (since := "2025-05-12")]
theorem hcomp {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (h₀ : Homotopic f₀ f₁) (h₁ : Homotopic g₀ g₁) :
    Homotopic (g₀.comp f₀) (g₁.comp f₁) :=
  h₁.comp h₀

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