preservesMonomorphisms_of_preservesLimitsOfShape

English

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

Русский

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

LaTeX

$$[PreservesMonomorphisms F]$$

Lean4

instance (priority := 100) preservesMonomorphisms_of_preservesLimitsOfShape [PreservesLimitsOfShape WalkingCospan F] :
    F.PreservesMonomorphisms where preserves f _ := preserves_mono_of_preservesLimit F f

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