instSupHomClass

Mathlib.Order.Hom.Lattice

URI: https://scilib.ai/kg/mathlib#SupHom.instSupHomClass

English

The SupHom class for the type of supremum-homomorphisms is defined whenever Max is available.

Русский

Определён класс SupHom для типа supremum-гомоморфизмов при условии наличия максимума.

LaTeX

$$$$ \mathrm{SupHomClass} (\mathrm{SupHom} \alpha \beta) \alpha \beta. $$$$

Lean4

instance : SupHomClass (SupHom α β) α β where map_sup := SupHom.map_sup'

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

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

Разделы

Аффилиация

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