English
If, for every x ∈ X, there exists an open partial homeomorphism e: X ⇢ Y with x in its source and f agrees with e on that source, then f is a local homeomorphism.
Русский
Если для каждого x ∈ X существует открытое частичное гомеоморфное отображение e: X ⇢ Y с x ∈ source(e) и f совпадает с e на source(e), то f — локальная гомеоморфия.
LaTeX
$$$\bigl(\forall x: X, \exists e: OpenPartialHomeomorph X Y, x \in e.source \wedge Set.EqOn f e e.source\bigr) \Rightarrow \operatorname{IsLocalHomeomorph}(f)$$$
Lean4
/-- Proves that `f` satisfies `IsLocalHomeomorph f`. The condition `h` is weaker than the
definition of `IsLocalHomeomorph f`, since it only requires `e : OpenPartialHomeomorph X Y` to
agree with `f` on its source `e.source`, as opposed to on the whole space `X`. -/
theorem mk (h : ∀ x : X, ∃ e : OpenPartialHomeomorph X Y, x ∈ e.source ∧ Set.EqOn f e e.source) : IsLocalHomeomorph f :=
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr (IsLocalHomeomorphOn.mk f Set.univ fun x _hx ↦ h x)
