instMono — Mathlib

English

If the underlying quiver is thin (at most one morphism between any two objects), then every morphism is mono.

Русский

Если ориентированная графа (квир) тонкая (не более одного морфизма между двумя объектами), то каждый морфизм является мономорфизмом.

LaTeX

$$$$\\operatorname{IsThin}(\\mathcal{C}) \\Rightarrow \\forall X,Y, f: X \\to Y, \\operatorname{Mono}(f).$$$$

Lean4

instance : Mono f where right_cancellation _ _ _ := Subsingleton.elim _ _

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