instSemilatticeSup

Mathlib.CategoryTheory.Sites.Coverage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Coverage.instSemilatticeSup

Lean4

instance : SemilatticeSup (Coverage C)
    where
  sup x
    y :=
    { coverings := fun B ↦ x B ∪ y B
      pullback := by
        rintro X Y f S (hx | hy)
        · obtain ⟨T, hT⟩ := x.pullback f S hx
          exact ⟨T, Or.inl hT.1, hT.2⟩
        · obtain ⟨T, hT⟩ := y.pullback f S hy
          exact ⟨T, Or.inr hT.1, hT.2⟩ }
  toPartialOrder := inferInstance
  le_sup_left _ _ _ := Set.subset_union_left
  le_sup_right _ _ _ := Set.subset_union_right
  sup_le _ _ _ hx hy X := Set.union_subset_iff.mpr ⟨hx X, hy X⟩

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

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

Разделы

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

Аффилиация

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