Borel

Mathlib.MeasureTheory.Category.MeasCat

URI: https://scilib.ai/kg/mathlib#Borel

Lean4

/-- The Borel functor, the canonical embedding of topological spaces into measurable spaces. -/
abbrev Borel : TopCat.{u} ⥤ MeasCat.{u} :=
  forget₂ TopCat.{u} MeasCat.{u}

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

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

Разделы

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

Аффилиация

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