instBotHomClass

Mathlib.Order.Hom.Bounded

URI: https://scilib.ai/kg/mathlib#BotHom.instBotHomClass

English

The class of bottom-preserving homomorphisms between base types carries the map_bot structure.

Русский

Класс гомоморфизмов снизу между базовыми типами несет структуру map_bot.

LaTeX

$$$\text{BotHomClass} (\text{BotHom } \alpha \beta) \alpha \beta$$$

Lean4

instance : BotHomClass (BotHom α β) α β where map_bot := BotHom.map_bot'

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

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

Разделы

Аффилиация

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