isEquivalence_preLeft — Mathlib

English

If F is an equivalence, then preLeft F L R is an equivalence.

Русский

Если F — эквивалентность, то preLeft F L R — эквивалентность.

LaTeX

$$$F \text{ IsEquivalence} \Rightarrow (\text{preLeft } F L R) \text{ IsEquivalence}.$$$

Lean4

/-- If `F` is an equivalence, then so is `preLeft F L R`. -/
instance isEquivalence_preLeft (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.IsEquivalence] : (preLeft F L R).IsEquivalence
    where

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