ofSheafCompHaus

Mathlib.Condensed.Explicit

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

Lean4

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

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

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

Разделы

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

Аффилиация

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