initial_of_empty_of_reflects — Mathlib

English

If ToType X is empty and forgetful preserves and reflects initial objects, then X is initial.

Русский

Если ToType X пуст и забывающий функтор сохраняет и отражает начальные, то X является начальным.

LaTeX

$$$ \\text{initial_of_empty_of_reflects } $$$

Lean4

/-- If `forget C` reflects initials and `ToType X` is empty, then `X` is initial. -/
theorem initial_of_empty_of_reflects [ReflectsColimit (Functor.empty.{0} C) (forget C)] (X : C)
    (h : IsEmpty (ToType X)) : Nonempty (IsInitial X) :=
  Nonempty.map (IsInitial.isInitialOfObj (forget C) _) <| (Types.initial_iff_empty (ToType X)).mpr h

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