instInfHomClass

Mathlib.Order.Hom.Lattice

URI: https://scilib.ai/kg/mathlib#InfHom.instInfHomClass

English

InfHomClass for InfHom α β is defined when α and β are lattices with Min.

Русский

InfHomClass для InfHom α β определяется, когда α и β — решетки с минимумом.

LaTeX

$$$$ \mathrm{InfHomClass} (\mathrm{InfHom} \alpha \beta) \alpha \beta. $$$$

Lean4

instance : InfHomClass (InfHom α β) α β where map_inf := InfHom.map_inf'

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

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

Разделы

Аффилиация

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