English
The glueing map fromOpenSubsetsGlue is an open map.
Русский
Отображение склейки fromOpenSubsetsGlue является открытым отображением.
LaTeX
$$fromOpenSubsetsGlue is an open map$$
Lean4
theorem fromOpenSubsetsGlue_isOpenMap : IsOpenMap (fromOpenSubsetsGlue U) :=
by
intro s hs
rw [(ofOpenSubsets U).isOpen_iff] at hs
rw [isOpen_iff_forall_mem_open]
rintro _ ⟨x, hx, rfl⟩
obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
use fromOpenSubsetsGlue U '' s ∩ Set.range (@Opens.inclusion' (TopCat.of α) (U i))
use Set.inter_subset_left
constructor
· rw [← Set.image_preimage_eq_inter_range]
apply (Opens.isOpenEmbedding (X := TopCat.of α) (U i)).isOpenMap
convert hs i using 1
rw [← ι_fromOpenSubsetsGlue, coe_comp, Set.preimage_comp]
congr! 1
exact Set.preimage_image_eq _ (fromOpenSubsetsGlue_injective U)
· refine ⟨Set.mem_image_of_mem _ hx, ?_⟩
rw [ι_fromOpenSubsetsGlue_apply]
exact Set.mem_range_self (f := (Opens.inclusion' _).hom) ⟨x, hx'⟩
