comp_left — Mathlib

English

If f is nullhomotopic, then composing on the left with f preserves nullhomotopy of f.

Русский

Если f нулеподобно гомотопирован, то композиция слева сохраняет нулеподобность.

LaTeX

$$$ \\forall f:\\,C(Y,Z),\\;f.Nullhomotopic \\to \\forall g:\\,C(X,Y), (f \\circ g).Nullhomotopic$$$

Lean4

theorem comp_left {f : C(Y, Z)} (hf : f.Nullhomotopic) (g : C(X, Y)) : (f.comp g).Nullhomotopic :=
  by
  obtain ⟨y, hy⟩ := hf
  use y
  exact .comp hy (.refl g)

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