isEquivalence_pre — Mathlib

English

If F is an equivalence, then the pre composition (pre F G S) is an equivalence.

Русский

Если F является эквивалентностью, то префиксная композиция (pre F G S) также эквивалентна.

LaTeX

$$$ \forall C D B (F: B\to C) (G: C\to D) (S: D), [F.IsEquivalence] \Rightarrow (\mathrm{pre}\ F\ G\ S).\mathrm{IsEquivalence}. $$$

Lean4

/-- If `F` is an equivalence, then so is the functor `(F ⋙ G, S) ⥤ (G, S)`. -/
instance isEquivalence_pre (F : B ⥤ C) (G : C ⥤ D) (S : D) [F.IsEquivalence] : (pre F G S).IsEquivalence :=
  Comma.isEquivalence_preLeft _ _ _

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