Theorems · Definition · general topology

OpenPartialHomeomorph.disjointUnion

{X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e e' : OpenPartialHomeomorph X Y) →
          [(x : X) → Decidable (x ∈ e.source)] →
            [(y : Y) → Decidable (y ∈ e.target)] →
              Disjoint e.source e'.source → Disjoint e.target e'.target → OpenPartialHomeomorph X Y

Combine two OpenPartialHomeomorphs with disjoint sources and disjoint targets. We reuse OpenPartialHomeomorph.piecewise then override toPartialEquiv to PartialEquiv.disjointUnion. This way we have better definitional equalities for source and target.

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceDecidableDecidable