isOpen_iff — Mathlib

English

An open subset U of the glued space corresponds exactly to the openness of its preimages under all gluing maps ι_i.

Русский

Открытость множества U в слитом пространстве эквивалентна открытости его предобразов под всеми вложениями ι_i.

LaTeX

$$$\text{IsOpen } U \;\iff\; \forall i, \text{IsOpen}(\iota_i^{-1}(U)).$$$

Lean4

theorem isOpen_iff (U : Set 𝖣.glued) : IsOpen U ↔ ∀ i, IsOpen (𝖣.ι i ⁻¹' U) :=
  by
  delta CategoryTheory.GlueData.ι
  simp_rw [← Multicoequalizer.ι_sigmaπ 𝖣.diagram]
  rw [← (homeoOfIso (Multicoequalizer.isoCoequalizer 𝖣.diagram).symm).isOpen_preimage]
  rw [coequalizer_isOpen_iff, colimit_isOpen_iff.{u}]
  tauto

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