Mathlib Map

Theorems · Definition · general topology

TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe

{X : Type u_1} →
  [inst : TopologicalSpace X] → (s : TopologicalSpace.Opens X) → Nonempty ↥s → OpenPartialHomeomorph (↥s) X

The inclusion of an open subset s of a space X into X is an open partial homeomorphism from the subtype s to X.

Defined in
Mathlib.Topology.OpenPartialHomeomorph.Basic
Cited by
8 results in Mathlib
Foundations
Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

OpenPartialHomeomorph.subtypeRestr · cited by 18OpenPartialHomeomorph.sub…TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target · cited by 4Opens.openPartialHomeomor…OpenPartialHomeomorph.subtypeRestr_def · cited by 1OpenPartialHomeomorph.sub…OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le · cited by 1OpenPartialHomeomorph.sub…OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr · cited by 1OpenPartialHomeomorph.sub…TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe · cited by 0Opens.openPartialHomeomor…TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source · cited by 0Opens.openPartialHomeomor…StructureGroupoid.restriction_mem_maximalAtlas_subtype · cited by 0StructureGroupoid.restric…TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe.congr_simp · cited by 0openPartialHomeomorphSubt…TopologicalSpace · cited by 24529TopologicalSpaceTopologicalSpace.Opens · cited by 2040TopologicalSpace.OpensOpenPartialHomeomorph · cited by 664OpenPartialHomeomorphTopology.IsOpenEmbedding.toOpenPartialHomeomorph · cited by 14IsOpenEmbedding.toOpenPar…Opens.openPartialHomeomorphSu…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by9

Results whose statement or proof uses this declaration.