instCoeFunForall

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#LowerAdjoint.instCoeFunForall

English

There is a canonical CoeFun instance for LowerAdjoint, turning it into a function type.

Русский

Существует канонический инстанс преобразования в функцию для LowerAdjoint, превращающий его в функцию.

LaTeX

$$$\\\\text{instance } : CoeFun (LowerAdjoint u) (\\\\urightarrow) \\\\text{ where } coe := toFun$$$

Lean4

instance : CoeFun (LowerAdjoint u) fun _ => α → β where coe := toFun

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

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

Разделы

Аффилиация

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