Theorems · Definition · general topology

OpenPartialHomeomorph.restr

{X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → Set X → OpenPartialHomeomorph X Y

Restricting an open partial homeomorphism e to e.source ∩ interior s. We use the interior to make sure that the restriction is well defined whatever the set s, since open partial homeomorphisms are by definition defined on open sets. In applications where s is open, this coincides with the restriction of partial equivalences.

Defined in

Mathlib.Topology.OpenPartialHomeomorph.IsImage

Cited by

47 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace