isLocalHomeomorph — Mathlib

English

Let f be a local diffeomorphism between manifolds; then f is a local homeomorphism.

Русский

Пусть f является локальным диффеоморфизмом между многообразиями; тогда f является локальным гомеоморфизмом.

LaTeX

$$$IsLocalDiffeomorph I J n f \Rightarrow IsLocalHomeomorph f$$$

Lean4

/-- A local diffeomorphism is a local homeomorphism. -/
theorem isLocalHomeomorph (hf : IsLocalDiffeomorph I J n f) : IsLocalHomeomorph f :=
  by
  rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ]
  rw [isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ] at hf
  exact hf.isLocalHomeomorphOn

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