toBotHomClass

Mathlib.Order.Hom.BoundedLattice

URI: https://scilib.ai/kg/mathlib#SupBotHomClass.toBotHomClass

← MathLib Explorer

English

From a SupBotHomClass, one obtains a BotHomClass.

Русский

Из класса SupBotHomClass следует класс BotHomClass.

LaTeX

$$$\operatorname{SupBotHomClass}(F,\alpha,\beta) \Rightarrow \operatorname{BotHomClass}(F,\alpha,\beta)$$$

Lean4

instance (priority := 100) toBotHomClass [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] : BotHomClass F α β :=
  { ‹SupBotHomClass F α β› with }
    -- See note [lower instance priority]

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

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

Разделы

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

Аффилиация

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