isSubterminal_of_mono_terminal_from

English

If the unique morphism from A to the terminal object is a monomorphism, A is subterminal. The converse of the previous fact.

Русский

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

LaTeX

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

Lean4

/-- If the unique morphism from `A` to the terminal object is a monomorphism, `A` is subterminal.
The converse of `IsSubterminal.mono_terminal_from`.
-/
theorem isSubterminal_of_mono_terminal_from [HasTerminal C] [Mono (terminal.from A)] : IsSubterminal A := fun Z f g =>
  by
  rw [← cancel_mono (terminal.from A)]
  subsingleton

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