instIsEquivalenceRightExtensionPostcomp₁OfIsIso

English

If G is an equivalence, then the postcomposition by f along G on the right side is an equivalence in the costructured arrow context.

Русский

Если G — эквивалентность, то посткомпозиция по f справа вдоль G эквивалентна в контексте CostructuredArrow.

LaTeX

$$$\text{RightExtension.postcomp₁ } G f F \text{ IsEquivalence}$$$

Lean4

noncomputable instance (f : L ⋙ G ⟶ L') [IsIso f] (F : C ⥤ H) : IsEquivalence (RightExtension.postcomp₁ G f F) := by
  apply CostructuredArrow.isEquivalenceMap₂

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