mono_isTerminal_from — Mathlib

English

If the unique morphism from A to a terminal object is a monomorphism, A is subterminal.

Русский

Если уникальный морфизм из A в терминальный объект является мономорфизмом, то A — субтерминальный объект.

LaTeX

$$$(\\text{mono from terminal})\\, A \\Rightarrow \\text{IsSubterminal } A$$$

Lean4

/-- If `A` is subterminal, the unique morphism from it to a terminal object is a monomorphism.
The converse of `isSubterminal_of_mono_isTerminal_from`.
-/
theorem mono_isTerminal_from (hA : IsSubterminal A) {T : C} (hT : IsTerminal T) : Mono (hT.from A) :=
  { right_cancellation := fun _ _ _ => hA _ _ }

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