Theorems · Definition · general topology

OpenPartialHomeomorph.piecewise

{X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e e' : OpenPartialHomeomorph X Y) →
          (s : Set X) →
            (t : Set Y) →
              [(x : X) → Decidable (x ∈ s)] →
                [(y : Y) → Decidable (y ∈ t)] →
                  e.IsImage s t →
                    e'.IsImage s t →
                      e.source ∩ frontier s = e'.source ∩ frontier s →
                        Set.EqOn (↑e) (↑e') (e.source ∩ frontier s) → OpenPartialHomeomorph X Y

Combine two OpenPartialHomeomorphs using Set.piecewise. The source of the new OpenPartialHomeomorph is s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s, and similarly for target. The function sends e.source ∩ s to e.target ∩ t using e and e'.source \ s to e'.target \ t using e', and similarly for the inverse function. To ensure the maps toFun and invFun are inverse of each other on the new source and target, the definition assumes that the sets s and t are related both by e.is_image and e'.is_image. To ensure that the new maps are continuous on source/target, it also assumes that e.source and e'.source meet frontier s on the same set and e x = e' x on this intersection.

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Constructions

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceDecidableDecidable