Theorems · Definition · general topology

OpenPartialHomeomorph.restrOpen

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

Restricting an open partial homeomorphism e to e.source ∩ s when s is open. This is sometimes hard to use because of the openness assumption, but it has the advantage that when it can be used then its PartialEquiv is defeq to PartialEquiv.restr.

Defined in

Mathlib.Topology.OpenPartialHomeomorph.IsImage

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace