mono_terminal_from — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `A` is subterminal, the unique morphism from it to the terminal object is a monomorphism.
The converse of `isSubterminal_of_mono_terminal_from`.
-/
theorem mono_terminal_from [HasTerminal C] (hA : IsSubterminal A) : Mono (terminal.from A) :=
  hA.mono_isTerminal_from terminalIsTerminal

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