Theorems · Theorem · general topology

OpenPartialHomeomorph.open_source

∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : OpenPartialHomeomorph X Y), IsOpen self.source

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Defs

Cited by

65 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace