diagram

Mathlib.Topology.Category.Profinite.AsLimit

URI: https://scilib.ai/kg/mathlib#Profinite.diagram

← MathLib Explorer

English

An abbreviation for X.fintypeDiagram ⋙ FintypeCat.toProfinite.

Русский

Сокращение: диаграмма X.fintypeDiagram ⋙ FintypeCat.toProfinite.

LaTeX

$$$\text{diagram}(X) = X.fintypeDiagram \circ \mathrm{FintypeCat.toProfinite}$$$

Lean4

/-- An abbreviation for `X.fintypeDiagram ⋙ FintypeCat.toProfinite`. -/
abbrev diagram : DiscreteQuotient X ⥤ Profinite :=
  X.fintypeDiagram ⋙ FintypeCat.toProfinite

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

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

Разделы

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

Аффилиация

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