continuous_symm_of_mem_pretrivializationAtlas

English

For any pretrivialization e in the atlas, the inverse map e.toPartialEquiv.symm is continuous on its target with respect to the total space topology.

Русский

Для любого e в атласе предтривиализации обратная карта e.toPartialEquiv.symm непрерывна на своей цели относительно топологии полного пространства.

LaTeX

$$$ \forall e \in a.pretrivializationAtlas,\; ContinuousOn(e.toPartialEquiv.symm, e.target)$$$

Lean4

theorem continuous_symm_of_mem_pretrivializationAtlas (he : e ∈ a.pretrivializationAtlas) :
    @ContinuousOn _ _ _ a.totalSpaceTopology e.toPartialEquiv.symm e.target :=
  by
  refine fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono ?_) U h)
  exact le_iSup₂ (α := TopologicalSpace (TotalSpace F E)) e he

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