of_continuous_injective_isOpenMap

English

If f is continuous, injective, and IsOpenMap, then f is an IsOpenEmbedding.

Русский

Если f непрерывно, инъективно и является открытым отображением, то f — открытое вложение.

LaTeX

$$$ \text{Continuous } f \land \text{Injective } f \land \text{IsOpenMap } f \rightarrow \text{IsOpenEmbedding } f $$$

Lean4

theorem of_continuous_injective_isOpenMap (h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsOpenMap f) :
    IsOpenEmbedding f :=
  by
  simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *, and_true]
  exact fun x => le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

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