isOpenEmbedding_stereographic_symm

English

The inverse stereographic map (stereographic hv).symm is an open embedding, i.e., a homeomorphism onto its image with open range.

Русский

Обратная карта стереографической проекции stereographic hv.symm является открытым вложением: гомеоморфизм на своём образе с открытым множеством образа.

LaTeX

$$$\\text{Topology.IsOpenEmbedding}((\\text{stereographic } hv).\\text{symm})$$$

Lean4

theorem isOpenEmbedding_stereographic_symm (hv : ‖v‖ = 1) : Topology.IsOpenEmbedding (stereographic hv).symm :=
  (stereographic hv).symm.to_isOpenEmbedding (by simp)

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