trans — Mathlib

English

If f0 ≃_P f1 and f1 ≃_P' f2, then f0 ≃_{P.trans P'} f2.

Русский

Если f0 гомотопичны через P к f1, и f1 через P' к f2, тогда f0 гомотопичен через P.trans P' к f2.

LaTeX

$$$\text{RightHomotopyRel } f_0 f_1 \rightarrow \text{RightHomotopyRel } f_1 f_2 \rightarrow \text{RightHomotopyRel } f_0 f_2$$$

Lean4

/-- If `f₀ : X ⟶ Y` is homotopic to `f₁` relative to a path object `P`,
and `f₁` is homotopic to `f₂` relative to a good path object `P'`,
then `f₀` is homotopic to `f₂` relative to the path object `P.trans P'`
when `Y` is fibrant. -/
noncomputable abbrev trans [IsFibrant Y] {f₀ f₁ f₂ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁) {P' : PathObject Y} [P'.IsGood]
    (h' : P'.RightHomotopy f₁ f₂) [HasPullback P.p₁ P'.p₀] : (P.trans P').RightHomotopy f₀ f₂ :=
  PrepathObject.RightHomotopy.trans h h'

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