colimit_isOpen_iff — Mathlib

English

For a subset U of the carrier of the colimit, U is open iff each preimage under colimit.ι F j is open in the corresponding F.obj j.

Русский

Для подмножества U носителя колимита верно: U открыто тогда и только тогда, когда прообраз по каждому colimit.ι F j открыт во внутреннем пространстве F.obj j.

LaTeX

$$$ \text{IsOpen } U \iff \forall j, \ IsOpen (\mathrm{colimit.ι} F j^{-1}(U)) $$$

Lean4

theorem colimit_isOpen_iff (F : J ⥤ TopCat.{u}) [HasColimit F] (U : Set ((colimit F : _) : Type u)) :
    IsOpen U ↔ ∀ j, IsOpen (colimit.ι F j ⁻¹' U) := by apply isOpen_iff_of_isColimit _ (colimit.isColimit _)

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