isClosed_iff_of_isColimit — Mathlib

English

In TopCat, a subset X of the carrier is closed iff all its preimages along the cocone maps are closed.

Русский

В TopCat подмножество X множества носителя замкнуто тогда и только тогда, когда все предобразования по отображениям конуса замкнуты.

LaTeX

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

Lean4

theorem isClosed_iff_of_isColimit (X : Set c.pt) : IsClosed X ↔ ∀ (j : J), IsClosed (c.ι.app j ⁻¹' X) := by
  simp only [← isOpen_compl_iff, isOpen_iff_of_isColimit _ hc, Functor.const_obj_obj, Set.preimage_compl]

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