restrictIndex

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreZeroHypercover.restrictIndex

Lean4

/-- Restrict the indexing type to `ι` by precomposing with a function `ι → E.I₀`. -/
@[simps]
def restrictIndex (E : PreZeroHypercover.{w} T) {ι : Type w'} (f : ι → E.I₀) : PreZeroHypercover.{w'} T
    where
  I₀ := ι
  X := E.X ∘ f
  f i := E.f (f i)

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

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

Разделы

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

Аффилиация

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