Theorems · Definition · general topology

OpenPartialHomeomorph.lift_openEmbedding

{X : Type u_7} →
  {X' : Type u_8} →
    {Z : Type u_9} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace X'] →
          [inst_2 : TopologicalSpace Z] →
            [Nonempty Z] →
              {f : X → X'} → OpenPartialHomeomorph X Z → Topology.IsOpenEmbedding f → OpenPartialHomeomorph X' Z

Extend an open partial homeomorphism e : X → Z to X' → Z, using an open embedding ι : X → X'. On ι(X), the extension is specified by e; its value elsewhere is arbitrary (and uninteresting).

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Constructions

Cited by

14 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceNonempty