ofSheafProfinite

Mathlib.Condensed.Explicit

URI: https://scilib.ai/kg/mathlib#CondensedSet.ofSheafProfinite

Lean4

/-- A `CondensedSet` version of `Condensed.ofSheafProfinite`. -/
noncomputable abbrev ofSheafProfinite (F : Profinite.{u}ᵒᵖ ⥤ Type (u + 1)) [PreservesFiniteProducts F]
    (hF : EqualizerCondition F) : CondensedSet :=
  Condensed.ofSheafProfinite F hF

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

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

Разделы

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

Аффилиация

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