instOrderBotToTypeOrdSmallObjectκ

Mathlib.CategoryTheory.SmallObject.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.instOrderBotToTypeOrdSmallObjectκ

English

There is a bottom element on the type I.smallObjectκ equipped with an order relation.

Русский

У типа I.smallObjectκ существует нижний элемент с заданной порядковой связью.

LaTeX

$$OrderBot I.smallObjectκ.ord.toType$$

Lean4

noncomputable instance : OrderBot I.smallObjectκ.ord.toType :=
  HasSmallObjectArgument.exists_cardinal.choose_spec.choose_spec.choose

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

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

Разделы

Аффилиация

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