comp_right — Mathlib

English

If f is nullhomotopic and g is any map Y→Z, then g∘f is nullhomotopic.

Русский

Если f нулеподобно гомотопированно и g: Y→Z произвольна, то g∘f нулеподобно гомотопирован.

LaTeX

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

Lean4

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

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