Theorems · Definition · general topology

IsLocalHomeomorphOn

{X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Set X → Prop

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.

Defined in

Mathlib.Topology.IsLocalHomeomorph

Cited by

22 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace