isLocalHomeomorph_iff_isOpenEmbedding_restrict

English

A function is a local homeomorph iff for every x, there exists an open neighborhood U of x such that U.restrict f is an open embedding.

Русский

Функция является локальным гомеоморфизмом тогда и только тогда, когда для каждого x существует открытое окрестность U, где U.restrict f является открытым вложением.

LaTeX

$$$IsLocalHomeomorph f \\iff \\forall x, \\exists U \\in 𝓝 x, IsOpenEmbedding (U.restrict f)$$$

Lean4

theorem isLocalHomeomorph_iff_isOpenEmbedding_restrict {f : X → Y} :
    IsLocalHomeomorph f ↔ ∀ x : X, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f) := by
  simp_rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ, isLocalHomeomorphOn_iff_isOpenEmbedding_restrict,
    imp_iff_right (Set.mem_univ _)]

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