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