Theorems · Definition · general topology

Homeomorph.transOpenPartialHomeomorph

{X : Type u_1} →
  {Y : Type u_3} →
    {Z : Type u_5} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] → X ≃ₜ Y → OpenPartialHomeomorph Y Z → OpenPartialHomeomorph X Z

Precompose an open partial homeomorphism with a homeomorphism. We modify the source and target to have better definitional behavior.

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Composition

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace