isLocallyInjective_iff_isOpenMap — Mathlib

English

IsLocallyInjective f is equivalent to the pullback map being an open map.

Русский

Локально инъективное отображение эквивалентно тому, что вытягиваемое отображение открыто.

LaTeX

$$IsLocallyInjective f \iff IsOpenMap (toPullbackDiag f)$$

Lean4

theorem isLocallyInjective_iff_isOpenMap {f : X → Y} : IsLocallyInjective f ↔ IsOpenMap (toPullbackDiag f) :=
  IsLocallyInjective_iff_isOpenEmbedding.trans
    ⟨IsOpenEmbedding.isOpenMap,
      .of_continuous_injective_isOpenMap (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩

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