instLE

Mathlib.Order.Hom.Bounded

URI: https://scilib.ai/kg/mathlib#TopHom.instLE

Lean4

instance instLE [LE β] [Top β] : LE (TopHom α β) where le f g := (f : α → β) ≤ g

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

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

Разделы

Аффилиация

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