isOpenEmbedding_iff_continuous_injective_isOpenMap

English

IsOpenEmbedding f is equivalent to Continuous f and Injective f and IsOpenMap f.

Русский

IsOpenEmbedding f эквивалентно Continuous f и Injective f и IsOpenMap f.

LaTeX

$$$ \text{IsOpenEmbedding } f \iff ( \text{Continuous } f \land \text{Injective } f \land \text{IsOpenMap } f ) $$$

Lean4

theorem isOpenEmbedding_iff_continuous_injective_isOpenMap :
    IsOpenEmbedding f ↔ Continuous f ∧ Injective f ∧ IsOpenMap f :=
  ⟨fun h => ⟨h.continuous, h.injective, h.isOpenMap⟩, fun h => .of_continuous_injective_isOpenMap h.1 h.2.1 h.2.2⟩

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