fromGlued_open_map — Mathlib

English

FromGlued is an open immersion.

Русский

FromGlued является открытым внедрением.

LaTeX

$$$$ \text{FromGlued} \text{ is an open immersion}. $$$$

Lean4

theorem fromGlued_open_map : IsOpenMap 𝒰.fromGlued.base :=
  by
  intro U hU
  rw [isOpen_iff_forall_mem_open]
  intro x hx
  rw [𝒰.gluedCover.isOpen_iff] at hU
  use 𝒰.fromGlued.base '' U ∩ Set.range (𝒰.f (𝒰.idx x)).base
  use Set.inter_subset_left
  constructor
  · rw [← Set.image_preimage_eq_inter_range]
    apply (show IsOpenImmersion (𝒰.f (𝒰.idx x)) from inferInstance).base_open.isOpenMap
    convert hU (𝒰.idx x) using 1
    simp only [← ι_fromGlued, gluedCover_U, comp_coeBase, TopCat.hom_comp, ContinuousMap.coe_comp, Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ 𝒰.fromGlued_injective
  · exact ⟨hx, 𝒰.covers x⟩

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