Theorems · Theorem · general topology

OpenPartialHomeomorph.piecewise_toPartialHomeomorph

∀ {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) [inst_2 : (x : X) → Decidable (x ∈ s)]
  [inst_3 : (y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
  (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)),
  (e.piecewise e' s t H H' Hs Heq).toPartialHomeomorph =
    { toPartialEquiv := e.piecewise e'.toPartialEquiv s t H H', continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

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