I₁'

Mathlib.CategoryTheory.Sites.Hypercover.One

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreOneHypercover.I₁'

Lean4

/-- The sigma type of all `E.I₁ i₁ i₂` for `⟨i₁, i₂⟩ : E.I₀ × E.I₀`. -/
abbrev I₁' : Type w :=
  Sigma (fun (i : E.I₀ × E.I₀) => E.I₁ i.1 i.2)

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

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

Разделы

Аффилиация

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