not_initial_of_inhabited

Mathlib.CategoryTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.not_initial_of_inhabited

← MathLib Explorer

English

If the fiber of X is inhabited, then X is not initial.

Русский

Если фибер X непуст, то X не начальный.

LaTeX

$$$\\forall X\\,\\forall x:\\,\\mathrm{F.obj}(X)\\text{ carrier},\\;\\mathrm{IsInitial}(X)\\Rightarrow \\mathrm{False}$$$

Lean4

/-- An object whose fiber is inhabited is not initial. -/
theorem not_initial_of_inhabited {X : C} (x : F.obj X) (h : IsInitial X) : False :=
  ((initial_iff_fiber_empty F X).mp ⟨h⟩).false x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru