isOpen_iff_of_isColimit — Mathlib

English

Let X be a subset of the carrier of c.pt. Then X is open in the colimit cocone topology iff for every j, the preimage under c.ι.app j of X is open in F.obj j.

Русский

Пусть X ⊆ носитель точки кокона c.pt. Тогда X открыто в топологии кокона колимита тогда и только тогда, когда прообраз X по каждому c.ι.app j открыт в соответствующем пространстве F.obj j.

LaTeX

$$$ IsOpen X \iff \forall j, IsOpen (c.ι.app j^{-1}(X)) $$$

Lean4

theorem isOpen_iff_of_isColimit (X : Set c.pt) : IsOpen X ↔ ∀ (j : J), IsOpen (c.ι.app j ⁻¹' X) :=
  by
  trans (⨆ (j : J), (F.obj j).str.coinduced (c.ι.app j)).IsOpen X
  · rw [← coinduced_of_isColimit c hc, isOpen_fold]
  · simp only [← isOpen_coinduced]
    apply isOpen_iSup_iff

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