trans — Mathlib

English

If f is Rel-homotopic to g and g to h (relative to S), then f is Rel-homotopic to h (relative to S).

Русский

Если f гомотопно относительно g по S и g относительно h по S, то f гомотопно относительно h по S.

LaTeX

$$$ \\forall f,g,h:\\,C(X,Y),\\;HomotopicRel(f,g,S) \\to HomotopicRel(g,h,S) \\to HomotopicRel(f,h,S)$$$

Lean4

@[trans]
theorem trans ⦃f g h : C(X, Y)⦄ (h₀ : HomotopicRel f g S) (h₁ : HomotopicRel g h S) : HomotopicRel f h S :=
  h₀.map2 HomotopyRel.trans h₁

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