non_zero_card_fiber_of_not_initial

English

If X is not initial (in the sense described), then the fiber cardinality is nonzero.

Русский

Если X не является исходным объектом, то кардинальность фибера не равна нулю.

LaTeX

$$$ Nat.card (F.obj X) \neq 0$$$

Lean4

/-- The cardinality of the fiber of a not-initial object is non-zero. -/
theorem non_zero_card_fiber_of_not_initial (X : C) (h : IsInitial X → False) : Nat.card (F.obj X) ≠ 0 :=
  by
  intro hzero
  refine Nonempty.elim ?_ h
  rw [initial_iff_fiber_empty F]
  exact Finite.card_eq_zero_iff.mp hzero

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