instNonemptyStructuredArrow

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Final.instNonemptyStructuredArrow

English

For every object d of D, the structured arrow (d ↓ F) is nonempty when F is final.

Русский

Для каждого объекта d в D категория структурированных стрелок (d ↓ F) непустая, если F финален.

LaTeX

$$$$ \forall d, \operatorname{Nonempty}\bigl(\operatorname{StructuredArrow}(d, F)\bigr). $$$$

Lean4

instance (d : D) : Nonempty (StructuredArrow d F) :=
  IsConnected.is_nonempty

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

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

Разделы

Аффилиация

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