toLocallyBoundedMap

Mathlib.Topology.Bornology.Hom

URI: https://scilib.ai/kg/mathlib#LocallyBoundedMapClass.toLocallyBoundedMap

Lean4

/-- Turn an element of a type `F` satisfying `LocallyBoundedMapClass F α β` into an actual
`LocallyBoundedMap`. This is declared as the default coercion from `F` to
`LocallyBoundedMap α β`. -/
@[coe]
def toLocallyBoundedMap [Bornology α] [Bornology β] [LocallyBoundedMapClass F α β] (f : F) : LocallyBoundedMap α β
    where
  toFun := f
  comap_cobounded_le' := comap_cobounded_le f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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