isOpen_iff_of_isColimit_cofork — Mathlib

English

For a cofork c with IsColimit hc, an open set U in c.pt is open if and only if its preimage under the projection c.π is open in the domain space. This expresses that the topology on the colimit is the quotient topology.

Русский

Для кофорка c с IsColimit hc множество U ⊆ c.pt открыто тогда и только тогда, когда его предобраз под отображением c.π открыто в исходном пространстве. Это выражает, что топология на координате-коллативе совпадает с факторной топологией.

LaTeX

$$$\\IsOpen U \\iff \\IsOpen (c.\\pi^{-1} U)$$$

Lean4

theorem isOpen_iff_of_isColimit_cofork (c : Cofork f g) (hc : IsColimit c) (U : Set c.pt) :
    IsOpen U ↔ IsOpen (c.π ⁻¹' U) := by
  rw [isOpen_iff_of_isColimit _ hc]
  constructor
  · intro h
    exact h .one
  · rintro h (_ | _)
    · rw [← c.w .left]
      exact Continuous.isOpen_preimage f.hom.continuous (c.π ⁻¹' U) h
    · exact h

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