of_initial — Mathlib

English

A category C is an InitialMonoClass if and only if every morphism out of the initial object is a mono.

Русский

Класс InitialMonoClass для категории C эквивалентен тому, что каждый морфизм из начального объекта моно.

LaTeX

$$$$\\big(\\forall X:\\, C,\\; \\mathrm{Mono}(\\mathrm{initial.to}\\,X)\\big) \\;\\Rightarrow\\; \\mathrm{InitialMonoClass}\\,C.$$$$

Lean4

/-- To show a category is an `InitialMonoClass` it suffices to show every morphism out of the
initial object is a monomorphism. -/
theorem of_initial [HasInitial C] (h : ∀ X : C, Mono (initial.to X)) : InitialMonoClass C :=
  InitialMonoClass.of_isInitial initialIsInitial h

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