nonempty_fiber_of_isConnected — Mathlib

English

The fiber of a connected object is nonempty.

Русский

Фибер связного объекта непуст.

LaTeX

$$$\\forall X\\,[\\mathrm{IsConnected}(X) \\Rightarrow \\mathrm{Nonempty}(\\mathrm{F.obj}(X).\\text{carrier})]$$$

Lean4

/-- The fiber of a connected object is nonempty. -/
instance nonempty_fiber_of_isConnected (X : C) [IsConnected X] : Nonempty (F.obj X) :=
  by
  by_contra h
  have ⟨hin⟩ : Nonempty (IsInitial X) := (initial_iff_fiber_empty F X).mpr (not_nonempty_iff.mp h)
  exact IsConnected.notInitial hin

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