Theorems · Theorem · general topology

OpenPartialHomeomorph.prod_toPartialHomeomorph

∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'),
  (eX.prod eY).toPartialHomeomorph =
    { toPartialEquiv := eX.prod eY.toPartialEquiv, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Constructions

Cited by

13 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpace