isOpenEmbedding_restrict — Mathlib

English

Restriction of an OpenPartialHomeomorph to a subset yields a homeomorphism on that subset; its restriction maps are open embeddings.

Русский

Ограничение OpenPartialHomeomorph к подмножеству образует гомеоморфизм на этом подмножестве; его ограничение образует открытые вложения.

LaTeX

$$$IsOpenEmbedding (e.source.restrict e) $$$

Lean4

theorem isOpenEmbedding_restrict : IsOpenEmbedding (e.source.restrict e) :=
  by
  refine
    .of_continuous_injective_isOpenMap (e.continuousOn.comp_continuous continuous_subtype_val Subtype.prop)
      e.injOn.injective fun V hV ↦ ?_
  rw [Set.restrict_eq, Set.image_comp]
  exact e.isOpen_image_of_subset_source (e.open_source.isOpenMap_subtype_val V hV) fun _ ⟨x, _, h⟩ ↦ h ▸ x.2

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