comp — Mathlib

English

If F: f0 ~ f1 is a Homotopy and G: g0 ~ g1 is a Homotopy, then their composition G ∘ F is a Homotopy from g0 ∘ f0 to g1 ∘ f1.

Русский

Если F: f0 ~ f1 и G: g0 ~ g1 — гомотопии, то композиция G ∘ F задаёт гомотопию между g0 ∘ f0 и g1 ∘ f1.

LaTeX

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

Lean4

/-- If we have a `Homotopy g₀ g₁` and a `Homotopy f₀ f₁`, then we can compose them and get a
`Homotopy (g₀.comp f₀) (g₁.comp f₁)`.
-/
@[simps]
def comp {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) :
    Homotopy (g₀.comp f₀) (g₁.comp f₁) where
  toFun x := G (x.1, F x)
  map_zero_left := by simp
  map_one_left := by simp

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