mono_of_mono_right — Mathlib

English

If f.right is mono, then f is mono in StructuredArrow provided certain functorial conditions hold.

Русский

Если правый компонент f.right моно, то f моно в StructuredArrow при определённых условиях на функтор.

LaTeX

$$$\text{If } f.right \text{ is mono, then } f \text{ is mono in StructuredArrow}$$$

Lean4

/-- The converse of this is true with additional assumptions, see `mono_iff_mono_right`. -/
theorem mono_of_mono_right {A B : StructuredArrow S T} (f : A ⟶ B) [h : Mono f.right] : Mono f :=
  (proj S T).mono_of_mono_map h

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