mono_from — Mathlib

English

To show a category is an InitialMonoClass it suffices to have an initial object I such that every morphism I → X is mono.

Русский

Чтобы доказать, что категория является InitialMonoClass, достаточно иметь начальнй объект I, из которого каждый морфизм I → X моно.

LaTeX

$$$(\\text{IsInitial } I) \\wedge (\\forall X, \\text{Mono} (I\\to X)) \\Rightarrow \\text{InitialMonoClass } C$$$

Lean4

theorem mono_from [InitialMonoClass C] {I} {X : C} (hI : IsInitial I) (f : I ⟶ X) : Mono f :=
  by
  rw [hI.hom_ext f (hI.to X)]
  apply InitialMonoClass.isInitial_mono_from

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