not_initial_iff_fiber_nonempty — Mathlib

English

Not initial is equivalent to having a nonempty fiber.

Русский

Не начальный эквивалентен непустому фиберу.

LaTeX

$$$(\\mathrm{IsInitial}(X) \\rightarrow \\mathrm{False}) \\iff \\mathrm{Nonempty}(\\mathrm{F.obj}(X))$$$

Lean4

/-- An object is not initial if and only if its fiber is nonempty. -/
theorem not_initial_iff_fiber_nonempty (X : C) : (IsInitial X → False) ↔ Nonempty (F.obj X) :=
  by
  rw [← not_isEmpty_iff]
  refine ⟨fun h he ↦ ?_, fun h hin ↦ h <| (initial_iff_fiber_empty F X).mp ⟨hin⟩⟩
  exact Nonempty.elim ((initial_iff_fiber_empty F X).mpr he) h

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