Basic

📁 Source: Mathlib/Topology/OpenPartialHomeomorph/Basic.lean

Statistics

Metric	Count
Definitions `homeomorphOfImageSubsetSource`, `ofContinuousOpen`, `ofContinuousOpenRestrict`, `refl`, `toHomeomorphOfSourceEqUnivTargetEqUniv`, `toHomeomorphSourceTarget`, `openPartialHomeomorphSubtypeCoe`, `partialHomeomorphSubtypeCoe`, `toOpenPartialHomeomorph`, `toPartialHomeomorph`	10
Theorems `coe_ofContinuousOpen`, `coe_ofContinuousOpenRestrict`, `coe_ofContinuousOpenRestrict_symm`, `coe_ofContinuousOpen_symm`, `homeomorphOfImageSubsetSource_apply`, `homeomorphOfImageSubsetSource_symm_apply`, `image_eq_target_inter_inv_preimage`, `image_source_eq_target`, `image_source_inter_eq`, `image_source_inter_eq'`, `isOpenEmbedding_restrict`, `isOpen_image_iff_of_subset_source`, `isOpen_image_of_subset_source`, `isOpen_image_source_inter`, `isOpen_image_symm_of_subset_target`, `isOpen_inter_preimage`, `isOpen_inter_preimage_symm`, `isOpen_symm_image_iff_of_subset_target`, `nhds_eq_comap_inf_principal`, `ofContinuousOpenRestrict_toPartialEquiv`, `ofContinuousOpen_toPartialEquiv`, `refl_apply`, `refl_partialEquiv`, `refl_source`, `refl_symm`, `refl_target`, `secondCountableTopology_source`, `source_inter_preimage_inv_preimage`, `source_inter_preimage_target_inter`, `source_preimage_target`, `symm_image_eq_source_inter_preimage`, `symm_image_target_eq_source`, `symm_image_target_inter_eq`, `target_inter_inv_preimage_preimage`, `toHomeomorphOfSourceEqUnivTargetEqUniv_apply`, `toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply`, `toHomeomorphSourceTarget_apply_coe`, `toHomeomorphSourceTarget_symm_apply_coe`, `to_isOpenEmbedding`, `openPartialHomeomorphSubtypeCoe_coe`, `openPartialHomeomorphSubtypeCoe_source`, `openPartialHomeomorphSubtypeCoe_target`, `partialHomeomorphSubtypeCoe_coe`, `partialHomeomorphSubtypeCoe_source`, `partialHomeomorphSubtypeCoe_target`, `toOpenPartialHomeomorph_apply`, `toOpenPartialHomeomorph_left_inv`, `toOpenPartialHomeomorph_right_inv`, `toOpenPartialHomeomorph_source`, `toOpenPartialHomeomorph_target`, `toPartialHomeomorph_left_inv`, `toPartialHomeomorph_right_inv`	52
Total	62

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
`homeomorphOfImageSubsetSource` 📖	CompOp	2 math math: `homeomorphOfImageSubsetSource_symm_apply`, `homeomorphOfImageSubsetSource_apply`
`ofContinuousOpen` 📖	CompOp	3 math math: `ofContinuousOpen_toPartialEquiv`, `coe_ofContinuousOpen_symm`, `coe_ofContinuousOpen`
`ofContinuousOpenRestrict` 📖	CompOp	3 math math: `coe_ofContinuousOpenRestrict_symm`, `ofContinuousOpenRestrict_toPartialEquiv`, `coe_ofContinuousOpenRestrict`
`refl` 📖	CompOp	18 math math: `trans_refl`, `StructureGroupoid.id_mem'`, `refl_partialEquiv`, `refl_apply`, `refl_prod_refl`, `FiberBundle.chartedSpace_chartAt`, `refl_symm`, `Homeomorph.refl_toOpenPartialHomeomorph`, `refl_source`, `chartedSpaceSelf_atlas`, `TangentBundle.chartAt`, `refl_target`, `Homeomorph.refl_toPartialHomeomorph`, `refl_trans`, `StructureGroupoid.id_mem`, `ofSet_univ_eq_refl`, `StructureGroupoid.id_mem_maximalAtlas`, `chartAt_self_eq`
`toHomeomorphOfSourceEqUnivTargetEqUniv` 📖	CompOp	2 math math: `toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply`, `toHomeomorphOfSourceEqUnivTargetEqUniv_apply`
`toHomeomorphSourceTarget` 📖	CompOp	4 math math: `toHomeomorphSourceTarget_apply_coe`, `StructureGroupoid.restriction_mem_maximalAtlas_subtype`, `toHomeomorphSourceTarget_symm_apply_coe`, `Homeomorph.unitBall_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofContinuousOpen` 📖	mathematical	`ContinuousOn` `PartialEquiv.toFun` `PartialEquiv.source` `IsOpenMap` `IsOpen`	`toFun'` `ofContinuousOpen`	—	—
`coe_ofContinuousOpenRestrict` 📖	mathematical	`ContinuousOn` `PartialEquiv.toFun` `PartialEquiv.source` `IsOpenMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `IsOpen`	`toFun'` `ofContinuousOpenRestrict`	—	—
`coe_ofContinuousOpenRestrict_symm` 📖	mathematical	`ContinuousOn` `PartialEquiv.toFun` `PartialEquiv.source` `IsOpenMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `IsOpen`	`toFun'` `symm` `ofContinuousOpenRestrict` `PartialEquiv.symm`	—	—
`coe_ofContinuousOpen_symm` 📖	mathematical	`ContinuousOn` `PartialEquiv.toFun` `PartialEquiv.source` `IsOpenMap` `IsOpen`	`toFun'` `symm` `ofContinuousOpen` `PartialEquiv.symm`	—	—
`homeomorphOfImageSubsetSource_apply` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv` `Set.image` `toFun'`	`DFunLike.coe` `Homeomorph` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphOfImageSubsetSource` `Set.MapsTo.restrict`	—	—
`homeomorphOfImageSubsetSource_symm_apply` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv` `Set.image` `toFun'`	`DFunLike.coe` `Homeomorph` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorphOfImageSubsetSource` `Set.MapsTo.restrict` `symm`	—	—
`image_eq_target_inter_inv_preimage` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv`	`Set.image` `toFun'` `Set.instInter` `PartialEquiv.target` `Set.preimage` `symm`	—	`PartialEquiv.image_eq_target_inter_inv_preimage`
`image_source_eq_target` 📖	mathematical	—	`Set.image` `toFun'` `PartialEquiv.source` `toPartialEquiv` `PartialEquiv.target`	—	`PartialEquiv.image_source_eq_target`
`image_source_inter_eq` 📖	mathematical	—	`Set.image` `toFun'` `Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `PartialEquiv.target` `Set.preimage` `symm`	—	`PartialEquiv.image_source_inter_eq`
`image_source_inter_eq'` 📖	mathematical	—	`Set.image` `toFun'` `Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `PartialEquiv.target` `Set.preimage` `symm`	—	`PartialEquiv.image_source_inter_eq'`
`isOpenEmbedding_restrict` 📖	mathematical	—	`Topology.IsOpenEmbedding` `Set.Elem` `PartialEquiv.source` `toPartialEquiv` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `toFun'`	—	`Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap` `ContinuousOn.comp_continuous` `continuousOn` `continuous_subtype_val` `Subtype.prop` `Set.InjOn.injective` `injOn` `Set.restrict_eq` `Set.image_comp` `isOpen_image_of_subset_source` `IsOpen.isOpenMap_subtype_val` `open_source`
`isOpen_image_iff_of_subset_source` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv`	`IsOpen` `Set.image` `toFun'`	—	`isOpen_symm_image_iff_of_subset_target` `symm_symm`
`isOpen_image_of_subset_source` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv`	`Set.image` `toFun'`	—	`image_eq_target_inter_inv_preimage` `ContinuousOn.isOpen_inter_preimage` `continuousOn_invFun` `open_target`
`isOpen_image_source_inter` 📖	mathematical	`IsOpen`	`Set.image` `toFun'` `Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv`	—	`isOpen_image_of_subset_source` `IsOpen.inter` `open_source` `Set.inter_subset_left`
`isOpen_image_symm_of_subset_target` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `PartialEquiv.target` `toPartialEquiv`	`Set.image` `toFun'` `symm`	—	`isOpen_image_of_subset_source` `symm_source`
`isOpen_inter_preimage` 📖	mathematical	`IsOpen`	`Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `Set.preimage` `toFun'`	—	`ContinuousOn.isOpen_inter_preimage` `continuousOn` `open_source`
`isOpen_inter_preimage_symm` 📖	mathematical	`IsOpen`	`Set` `Set.instInter` `PartialEquiv.target` `toPartialEquiv` `Set.preimage` `toFun'` `symm`	—	`ContinuousOn.isOpen_inter_preimage` `continuousOn` `open_target`
`isOpen_symm_image_iff_of_subset_target` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.target` `toPartialEquiv`	`IsOpen` `Set.image` `toFun'` `symm`	—	`symm_image_eq_source_inter_preimage` `Set.inter_subset_left` `PartialEquiv.image_symm_image_of_subset_target` `isOpen_image_of_subset_source`
`nhds_eq_comap_inf_principal` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`nhds` `Filter` `Filter.instInf` `Filter.comap` `toFun'` `Filter.principal`	—	`CanLift.prf` `Subtype.canLift` `IsOpen.nhdsWithin_eq` `open_source` `map_nhds_subtype_val` `Filter.map_comap_setCoe_val` `Homeomorph.nhds_eq_comap` `nhds_subtype_eq_comap` `Filter.comap_comap`
`ofContinuousOpenRestrict_toPartialEquiv` 📖	mathematical	`ContinuousOn` `PartialEquiv.toFun` `PartialEquiv.source` `IsOpenMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `IsOpen`	`toPartialEquiv` `ofContinuousOpenRestrict`	—	—
`ofContinuousOpen_toPartialEquiv` 📖	mathematical	`ContinuousOn` `PartialEquiv.toFun` `PartialEquiv.source` `IsOpenMap` `IsOpen`	`toPartialEquiv` `ofContinuousOpen`	—	—
`refl_apply` 📖	mathematical	—	`toFun'` `refl`	—	—
`refl_partialEquiv` 📖	mathematical	—	`toPartialEquiv` `refl` `PartialEquiv.refl`	—	—
`refl_source` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `refl` `Set.univ`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_target` 📖	mathematical	—	`PartialEquiv.target` `toPartialEquiv` `refl` `Set.univ`	—	—
`secondCountableTopology_source` 📖	mathematical	—	`SecondCountableTopology` `Set.Elem` `PartialEquiv.source` `toPartialEquiv` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Homeomorph.secondCountableTopology` `TopologicalSpace.Subtype.secondCountableTopology`
`source_inter_preimage_inv_preimage` 📖	mathematical	—	`Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `Set.preimage` `toFun'` `symm`	—	`PartialEquiv.source_inter_preimage_inv_preimage`
`source_inter_preimage_target_inter` 📖	mathematical	—	`Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `Set.preimage` `toFun'` `PartialEquiv.target`	—	`PartialEquiv.source_inter_preimage_target_inter`
`source_preimage_target` 📖	mathematical	—	`Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv` `Set.preimage` `toFun'` `PartialEquiv.target`	—	`mapsTo`
`symm_image_eq_source_inter_preimage` 📖	mathematical	`Set` `Set.instHasSubset` `PartialEquiv.target` `toPartialEquiv`	`Set.image` `toFun'` `symm` `Set.instInter` `PartialEquiv.source` `Set.preimage`	—	`image_eq_target_inter_inv_preimage`
`symm_image_target_eq_source` 📖	mathematical	—	`Set.image` `toFun'` `symm` `PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source`	—	`image_source_eq_target`
`symm_image_target_inter_eq` 📖	mathematical	—	`Set.image` `toFun'` `symm` `Set` `Set.instInter` `PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source` `Set.preimage`	—	`image_source_inter_eq`
`target_inter_inv_preimage_preimage` 📖	mathematical	—	`Set` `Set.instInter` `PartialEquiv.target` `toPartialEquiv` `Set.preimage` `toFun'` `symm`	—	`source_inter_preimage_inv_preimage`
`toHomeomorphOfSourceEqUnivTargetEqUniv_apply` 📖	mathematical	`PartialEquiv.source` `toPartialEquiv` `Set.univ` `PartialEquiv.target`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorphOfSourceEqUnivTargetEqUniv` `toFun'`	—	—
`toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply` 📖	mathematical	`PartialEquiv.source` `toPartialEquiv` `Set.univ` `PartialEquiv.target`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorphOfSourceEqUnivTargetEqUniv` `toFun'` `symm`	—	—
`toHomeomorphSourceTarget_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv` `DFunLike.coe` `Homeomorph` `Set.Elem` `PartialEquiv.source` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorphSourceTarget` `toFun'`	—	—
`toHomeomorphSourceTarget_symm_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv` `DFunLike.coe` `Homeomorph` `Set.Elem` `PartialEquiv.target` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorphSourceTarget` `toFun'` `symm`	—	—
`to_isOpenEmbedding` 📖	mathematical	`PartialEquiv.source` `toPartialEquiv` `Set.univ`	`Topology.IsOpenEmbedding` `toFun'`	—	`Topology.IsOpenEmbedding.comp` `isOpenEmbedding_restrict` `Homeomorph.isOpenEmbedding`

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
`openPartialHomeomorphSubtypeCoe` 📖	CompOp	7 math math: `partialHomeomorphSubtypeCoe_target`, `openPartialHomeomorphSubtypeCoe_coe`, `partialHomeomorphSubtypeCoe_coe`, `openPartialHomeomorphSubtypeCoe_target`, `openPartialHomeomorphSubtypeCoe_source`, `OpenPartialHomeomorph.subtypeRestr_def`, `partialHomeomorphSubtypeCoe_source`
`partialHomeomorphSubtypeCoe` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`openPartialHomeomorphSubtypeCoe_coe` 📖	mathematical	—	`OpenPartialHomeomorph.toFun'` `TopologicalSpace.Opens` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `openPartialHomeomorphSubtypeCoe`	—	—
`openPartialHomeomorphSubtypeCoe_source` 📖	mathematical	—	`PartialEquiv.source` `TopologicalSpace.Opens` `SetLike.instMembership` `instSetLike` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceSubtype` `openPartialHomeomorphSubtypeCoe` `Set.univ`	—	—
`openPartialHomeomorphSubtypeCoe_target` 📖	mathematical	—	`PartialEquiv.target` `TopologicalSpace.Opens` `SetLike.instMembership` `instSetLike` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceSubtype` `openPartialHomeomorphSubtypeCoe` `SetLike.coe`	—	`Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target` `Subtype.range_coe_subtype`
`partialHomeomorphSubtypeCoe_coe` 📖	mathematical	—	`OpenPartialHomeomorph.toFun'` `TopologicalSpace.Opens` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype` `openPartialHomeomorphSubtypeCoe`	—	`openPartialHomeomorphSubtypeCoe_coe`
`partialHomeomorphSubtypeCoe_source` 📖	mathematical	—	`PartialEquiv.source` `TopologicalSpace.Opens` `SetLike.instMembership` `instSetLike` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceSubtype` `openPartialHomeomorphSubtypeCoe` `Set.univ`	—	`openPartialHomeomorphSubtypeCoe_source`
`partialHomeomorphSubtypeCoe_target` 📖	mathematical	—	`PartialEquiv.target` `TopologicalSpace.Opens` `SetLike.instMembership` `instSetLike` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceSubtype` `openPartialHomeomorphSubtypeCoe` `SetLike.coe`	—	`openPartialHomeomorphSubtypeCoe_target`

Topology.IsOpenEmbedding

Definitions

Name	Category	Theorems
`toOpenPartialHomeomorph` 📖	CompOp	8 math math: `toOpenPartialHomeomorph_source`, `contMDiffOn_isOpenEmbedding_symm`, `toOpenPartialHomeomorph_apply`, `toPartialHomeomorph_left_inv`, `toOpenPartialHomeomorph_target`, `toOpenPartialHomeomorph_right_inv`, `toPartialHomeomorph_right_inv`, `toOpenPartialHomeomorph_left_inv`
`toPartialHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toOpenPartialHomeomorph_apply` 📖	mathematical	`Topology.IsOpenEmbedding`	`OpenPartialHomeomorph.toFun'` `toOpenPartialHomeomorph`	—	—
`toOpenPartialHomeomorph_left_inv` 📖	mathematical	`Topology.IsOpenEmbedding`	`OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph`	—	`toOpenPartialHomeomorph_apply` `OpenPartialHomeomorph.left_inv` `Set.mem_univ`
`toOpenPartialHomeomorph_right_inv` 📖	mathematical	`Topology.IsOpenEmbedding` `Set` `Set.instMembership` `Set.range`	`OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph`	—	`toOpenPartialHomeomorph_apply` `OpenPartialHomeomorph.right_inv` `toOpenPartialHomeomorph_target`
`toOpenPartialHomeomorph_source` 📖	mathematical	`Topology.IsOpenEmbedding`	`PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `toOpenPartialHomeomorph` `Set.univ`	—	—
`toOpenPartialHomeomorph_target` 📖	mathematical	`Topology.IsOpenEmbedding`	`PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `toOpenPartialHomeomorph` `Set.range`	—	`Set.image_univ`
`toPartialHomeomorph_left_inv` 📖	mathematical	`Topology.IsOpenEmbedding`	`OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph`	—	`toOpenPartialHomeomorph_left_inv`
`toPartialHomeomorph_right_inv` 📖	mathematical	`Topology.IsOpenEmbedding` `Set` `Set.instMembership` `Set.range`	`OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph`	—	`toOpenPartialHomeomorph_right_inv`

---

← Back to Index