isOpen_target_of_mem_pretrivializationAtlas_inter

English

For pretrivializations e,e' with e' in atlas, the set e'.target ∩ (e'.symm)^{-1}(e.source) is open.

Русский

Для предтривиализаций e,e' с принадлежностью e' к атласу, пересечение e'.target и предобраза через e'.symm от e.source открыто.

LaTeX

$$$ IsOpen( e'.target \cap (e'.toPartialEquiv.symm)^{-1} ( e.source ) ) $$$

Lean4

theorem isOpen_target_of_mem_pretrivializationAtlas_inter (e e' : Pretrivialization F (π F E))
    (he' : e' ∈ a.pretrivializationAtlas) : IsOpen (e'.toPartialEquiv.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source) :=
  by
  letI := a.totalSpaceTopology
  obtain ⟨u, hu1, hu2⟩ :=
    continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he') e.source (a.isOpen_source e)
  rw [inter_comm, hu2]
  exact hu1.inter e'.open_target

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