open_image_open — Mathlib

English

For each index i, the image of an open set under the i-th inclusion map into the glued space is open in the glued space.

Русский

Для каждого индекса i образ открытого множества под соответствующим включением в пространство склейки является открытым в этом пространстве.

LaTeX

$$$\\text{IsOpen}(\\iota_i''U)$$$

Lean4

theorem open_image_open (i : D.J) (U : Opens (𝖣.U i)) : IsOpen (𝖣.ι i '' U) :=
  by
  rw [isOpen_iff]
  intro j
  rw [preimage_image_eq_image]
  apply (D.f_open _ _).isOpenMap
  apply (D.t j i ≫ D.f i j).hom.continuous_toFun.isOpen_preimage
  exact U.isOpen

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