isSubterminal_of_mono_isTerminal_from

English

If the terminal morphism from A is mono, A is subterminal.

Русский

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

LaTeX

$$$\\text{Mono}(\\text{terminal.from } A) \\Rightarrow \\text{IsSubterminal } A$$$

Lean4

/-- If the unique morphism from `A` to a terminal object is a monomorphism, `A` is subterminal.
The converse of `IsSubterminal.mono_isTerminal_from`.
-/
theorem isSubterminal_of_mono_isTerminal_from {T : C} (hT : IsTerminal T) [Mono (hT.from A)] : IsSubterminal A :=
  fun Z f g => by
  rw [← cancel_mono (hT.from A)]
  apply hT.hom_ext

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