isEquivalence_toOver — Mathlib

English

If F is an equivalence, then the induced functor toOver F X is an equivalence.

Русский

Если F является эквиваленцией, то полученный функтор toOver(F,X) также является эквивалентностью.

LaTeX

$$$F \\text{ is an equivalence } \\Rightarrow (\\mathrm{toOver}(F,X)) \\text{ is an equivalence}.$$$

Lean4

/-- An equivalence `F` induces an equivalence `CostructuredArrow F X ≌ Over X`. -/
instance isEquivalence_toOver (F : D ⥤ T) (X : T) [F.IsEquivalence] : (toOver F X).IsEquivalence :=
  CostructuredArrow.isEquivalence_pre _ _ _

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