sum

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Precoverage.ZeroHypercover.sum

Lean4

/-- Disjoint union of two `0`-hypercovers. -/
@[simps toPreZeroHypercover]
def sum [J.IsStableUnderSup] (E : ZeroHypercover.{w} J S) (F : ZeroHypercover.{w'} J S) : ZeroHypercover.{max w w'} J S
    where
  __ := E.toPreZeroHypercover.sum F.toPreZeroHypercover
  mem₀ := by
    rw [PreZeroHypercover.presieve₀_sum]
    exact J.sup_mem_coverings E.mem₀ F.mem₀

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

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

Разделы

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

Аффилиация

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