opensLeCoverCocone — Mathlib

English

The category OpensLeCover U consists of opens contained in some U_i.

Русский

Категория OpensLeCover U состоит из открытых множеств, содержащихся в некоторых U_i.

LaTeX

$$$\text{OpensLeCover}(U)=\{V:\operatorname{Opens}(X)\mid \exists i, V\le U_i\}$$$

Lean4

/-- `iSup U` as a cocone over the opens sets contained in some element of the cover.

(In fact this is a colimit cocone.)
-/
def opensLeCoverCocone : Cocone (ObjectProperty.ι _ : OpensLeCover U ⥤ Opens X)
    where
  pt := iSup U
  ι := { app := fun V : OpensLeCover U => V.homToIndex ≫ Opens.leSupr U _ }

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