isOpenEmbedding_of_comp — Mathlib

English

Continuous local sections of a local homeomorphism are open embeddings.

Русский

Непрерывные локальные секции локального гомеоморфизма являются открытыми вложениями.

LaTeX

$$$\operatorname{IsLocalHomeomorph}(g) \Rightarrow \operatorname{IsOpenEmbedding}(g \circ f) \Rightarrow \operatorname{Continuous}(f) \Rightarrow \operatorname{IsOpenEmbedding}(f)$$$

Lean4

/-- Continuous local sections of a local homeomorphism are open embeddings. -/
theorem isOpenEmbedding_of_comp (hf : IsLocalHomeomorph g) (hgf : IsOpenEmbedding (g ∘ f)) (cont : Continuous f) :
    IsOpenEmbedding f :=
  (hgf.isLocalHomeomorph.of_comp hf cont).isOpenEmbedding_of_injective hgf.injective.of_comp

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