trans — Mathlib

English

Two good path objects can be glued to form a new path object for A.

Русский

Два хороших путь-объекта можно слепить в новый путь-объект для A.

LaTeX

$$$P.trans P' : PathObject(A)$$$

Lean4

/-- The gluing of two good path objects. -/
@[simps!]
noncomputable def trans [IsFibrant A] (P P' : PathObject A) [P'.IsGood] : PathObject A
    where
  __ := P.toPrepathObject.trans P'.toPrepathObject
  weakEquivalence_ι :=
    by
    have : WeakEquivalence (pullback.lift P.ι P'.ι (by simp) ≫ pullback.fst P.p₁ P'.p₀ ≫ P.p₀) :=
      by
      rw [pullback.lift_fst_assoc, PrepathObject.ι_p₀]
      infer_instance
    dsimp
    apply weakEquivalence_of_postcomp _ (pullback.fst P.p₁ P'.p₀ ≫ P.p₀)

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