isOpenEmbedding_of_injective — Mathlib

English

An injective local homeomorphism is an open embedding.

Русский

Инъективный локальный гомеоморфизм является открытым вложением.

LaTeX

$$$\\operatorname{IsLocalHomeomorph}(f) \\land f \\text{ injective} \\Rightarrow \\operatorname{IsOpenEmbedding}(f)$$$

Lean4

/-- An injective local homeomorphism is an open embedding. -/
theorem isOpenEmbedding_of_injective (hf : IsLocalHomeomorph f) (hi : f.Injective) : IsOpenEmbedding f :=
  .of_continuous_injective_isOpenMap hf.continuous hi hf.isOpenMap

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