reflectsMonomorphisms_of_reflectsLimitsOfShape

English

An instance asserts that F reflects monomorphisms when it reflects limits of shape WalkingCospan.

Русский

Инстанс утверждает, что F отражает мономорфизмы при отражении пределов формы WalkingCospan.

LaTeX

$$[ReflectsMonomorphisms F]$$

Lean4

instance (priority := 100) reflectsMonomorphisms_of_reflectsLimitsOfShape [ReflectsLimitsOfShape WalkingCospan F] :
    F.ReflectsMonomorphisms where reflects f _ := reflects_mono_of_reflectsLimit F f

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