comp — Mathlib

English

The function comp defines a Homotopy between the composed maps g0 ∘ f0 and g1 ∘ f1 from F and hf.

Русский

Определение comp задаёт гомотопию между составными отображениями g0 ∘ f0 и g1 ∘ f1 из F и hf.

LaTeX

$$$$ \text{comp: } f_0 \sim f_1, \ g_0 \sim g_1 \Rightarrow (g_0 \circ f_0) \sim (g_1 \circ f_1) $$$$

Lean4

theorem comp {g₀ g₁ : C(Y, Z)} {f₀ f₁ : C(X, Y)} (hg : Homotopic g₀ g₁) (hf : Homotopic f₀ f₁) :
    Homotopic (g₀.comp f₀) (g₁.comp f₁) :=
  hg.map2 Homotopy.comp hf

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