hasForgetToMeasCat

Mathlib.MeasureTheory.Category.MeasCat

URI: https://scilib.ai/kg/mathlib#TopCat.hasForgetToMeasCat

Lean4

instance hasForgetToMeasCat : HasForget₂ TopCat.{u} MeasCat.{u}
    where
  forget₂.obj X := @MeasCat.of _ (borel X)
  forget₂.map f := ⟨f.1, f.hom.2.borel_measurable⟩

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

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

Разделы

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

Аффилиация

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