isLocalHomeomorphOn — Mathlib

English

A local diffeomorphism on s is a local homeomorphism on s.

Русский

Локальный диффеоморфизм на s является локальным гомеоморфизмом на s.

LaTeX

$$$ IsLocalDiffeomorphOn I J n f s \to IsLocalHomeomorphOn f s $$$

Lean4

/-- A local diffeomorphism on `s` is a local homeomorphism on `s`. -/
theorem isLocalHomeomorphOn {s : Set M} (hf : IsLocalDiffeomorphOn I J n f s) : IsLocalHomeomorphOn f s :=
  by
  apply IsLocalHomeomorphOn.mk
  intro x hx
  choose U hyp using hf ⟨x, hx⟩
  exact ⟨U.toOpenPartialHomeomorph, hyp⟩

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