IsLocalHomeomorphOn — Mathlib

English

If for every x ∈ s there exists an OpenPartialHomeomorph e with x ∈ e.source and f agrees with e on e.source, then f is a local homeomorph on s.

Русский

Если для каждого x ∈ s существует открытое частичное гомеоморфизм e с x ∈ source(e) и f совпадает с e на source(e), тогда f — локальный гомеоморфизм на s.

LaTeX

$$$\\forall x \\in s, \\exists e:\\mathrm{OpenPartialHomeomorph}(X,Y), x\\in e.source \\land f|_{e.source}=e$$$

Lean4

/-- A function `f : X → Y` satisfies `IsLocalHomeomorphOn f s` if each `x ∈ s` is contained in
the source of some `e : OpenPartialHomeomorph X Y` with `f = e`. -/
def IsLocalHomeomorphOn :=
  ∀ x ∈ s, ∃ e : OpenPartialHomeomorph X Y, x ∈ e.source ∧ f = e

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