trans — Mathlib

English

The gluing of two good cylinders yields a cylinder; there is a weak equivalence on the projection π.

Русский

Слияние двух хороших цилиндров образует цилиндр; есть слабая эквивалентность проекции π.

LaTeX

$$$(P.trans P'.toPrecylinder).IsGood$ and $\text{WeakEquivalence}((P.trans P').\pi)$$$

Lean4

/-- The gluing of two good cylinders. -/
@[simps!]
noncomputable def trans [IsCofibrant A] (P P' : Cylinder A) [P'.IsGood] : Cylinder A
    where
  __ := P.toPrecylinder.trans P'.toPrecylinder
  weakEquivalence_π :=
    by
    have : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫ pushout.desc P.π P'.π (by simp)) :=
      by
      simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app, Precylinder.i₀_π]
      infer_instance
    dsimp
    apply weakEquivalence_of_precomp (P.i₀ ≫ pushout.inl _ _)

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