of_isEmbedding_isOpenMap — Mathlib

English

If f is an embedding and g is an open embedding, then g ∘ f is open embedding iff f is open embedding.

Русский

Если f — вложение, и g — открытое вложение, то g ∘ f является открытым вложением тогда и только тогда, когда f является открытым вложением.

LaTeX

$$$ \text{IsOpenEmbedding}(g \circ f) \iff \text{IsOpenEmbedding}(f) $$$

Lean4

theorem of_isEmbedding_isOpenMap (h₁ : IsEmbedding f) (h₂ : IsOpenMap f) : IsOpenEmbedding f :=
  ⟨h₁, h₂.isOpen_range⟩

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