instPartialOrder

Mathlib.CategoryTheory.Sites.Coverage

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

Lean4

instance : PartialOrder (Coverage C) where
  le A B := A.coverings ≤ B.coverings
  le_refl _ _ := le_refl _
  le_trans _ _ _ h1 h2 X := le_trans (h1 X) (h2 X)
  le_antisymm _ _ h1 h2 := Coverage.ext <| funext <| fun X => le_antisymm (h1 X) (h2 X)

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

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

Разделы

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

Аффилиация

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