IsLocallyInjective_iff_isOpenEmbedding

English

IsLocallyInjective f is equivalent to the pullback diagonal being an open embedding.

Русский

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

LaTeX

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

Lean4

theorem IsLocallyInjective_iff_isOpenEmbedding {f : X → Y} :
    IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f) :=
  by
  rw [isLocallyInjective_iff_isOpen_diagonal, ← range_toPullbackDiag]
  exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩

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