Constructions

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

Statistics

Metric	Count
Definitions const, disjointUnion, lift_openEmbedding, pi, piecewise, prod, subtypeRestr, transHomeomorph	8
Theorems const_apply, const_source, const_target, lift_openEmbedding_apply, lift_openEmbedding_source, lift_openEmbedding_symm, lift_openEmbedding_symm_source, lift_openEmbedding_symm_target, lift_openEmbedding_target, lift_openEmbedding_toFun, lift_openEmbedding_trans, lift_openEmbedding_trans_apply, map_subtype_source, pi_apply, pi_source, pi_symm_apply, pi_target, pi_toPartialEquiv, piecewise_apply, piecewise_toPartialEquiv, prod_apply, prod_eq_prod_of_nonempty, prod_eq_prod_of_nonempty', prod_source, prod_symm, prod_symm_apply, prod_symm_trans_prod, prod_target, prod_toPartialEquiv, prod_trans, refl_prod_refl, subtypeRestr_coe, subtypeRestr_def, subtypeRestr_source, subtypeRestr_symm_apply, subtypeRestr_symm_eqOn, subtypeRestr_symm_eqOn_of_le, subtypeRestr_symm_trans_subtypeRestr, subtypeRestr_target_subset, symm_piecewise, transHomeomorph_apply, transHomeomorph_eq_trans, transHomeomorph_source, transHomeomorph_symm_apply, transHomeomorph_target, transHomeomorph_transHomeomorph, trans_transHomeomorph	47
Total	55

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
const 📖	CompOp	4 math math: chartedSpace_of_discreteTopology_chartAt, const_target, const_source, const_apply
disjointUnion 📖	CompOp	—
lift_openEmbedding 📖	CompOp	12 math math: ChartedSpace.sum_chartAt_inr, lift_openEmbedding_toFun, lift_openEmbedding_trans_apply, lift_openEmbedding_source, ChartedSpace.sum_chartAt_inl, lift_openEmbedding_trans, lift_openEmbedding_symm, lift_openEmbedding_target, lift_openEmbedding_symm_target, lift_openEmbedding_symm_source, lift_openEmbedding_apply, ChartedSpace.mem_atlas_sum
pi 📖	CompOp	6 math math: pi_target, pi_source, pi_apply, pi_toPartialEquiv, pi_symm_apply, piChartedSpace_chartAt
piecewise 📖	CompOp	3 math math: symm_piecewise, piecewise_apply, piecewise_toPartialEquiv
prod 📖	CompOp	15 math math: prod_symm_apply, refl_prod_refl, FiberBundle.chartedSpace_chartAt, prod_target, prod_apply, prod_symm, prodChartedSpace_chartAt, prod_toPartialEquiv, TangentBundle.chartAt, prod_symm_trans_prod, extend_prod, IsManifold.mem_maximalAtlas_prod, prod_source, prod_trans, contDiffGroupoid_prod
subtypeRestr 📖	CompOp	14 math math: map_subtype_source, subtypeRestr_symm_trans_subtypeRestr, TopologicalSpace.Opens.chartAt_eq, subtypeRestr_coe, TopologicalSpace.Opens.chart_eq', TopologicalSpace.Opens.chart_eq, StructureGroupoid.trans_restricted, StructureGroupoid.restriction_in_maximalAtlas, subtypeRestr_symm_eqOn, subtypeRestr_def, subtypeRestr_target_subset, subtypeRestr_symm_eqOn_of_le, StructureGroupoid.subtypeRestr_mem_maximalAtlas, subtypeRestr_source
transHomeomorph 📖	CompOp	7 math math: transHomeomorph_source, transHomeomorph_symm_apply, transHomeomorph_target, trans_transHomeomorph, transHomeomorph_transHomeomorph, transHomeomorph_apply, transHomeomorph_eq_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_apply 📖	mathematical	IsOpen Set Set.instSingletonSet	toFun' const	—	—
const_source 📖	mathematical	IsOpen Set Set.instSingletonSet	PartialEquiv.source toPartialEquiv const	—	—
const_target 📖	mathematical	IsOpen Set Set.instSingletonSet	PartialEquiv.target toPartialEquiv const	—	—
lift_openEmbedding_apply 📖	mathematical	Topology.IsOpenEmbedding	toFun' lift_openEmbedding	—	lift_openEmbedding_toFun Function.Injective.extend_apply Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding
lift_openEmbedding_source 📖	mathematical	Topology.IsOpenEmbedding	PartialEquiv.source toPartialEquiv lift_openEmbedding Set.image	—	—
lift_openEmbedding_symm 📖	mathematical	Topology.IsOpenEmbedding	toFun' symm lift_openEmbedding	—	—
lift_openEmbedding_symm_source 📖	mathematical	Topology.IsOpenEmbedding	PartialEquiv.source toPartialEquiv symm lift_openEmbedding PartialEquiv.target	—	—
lift_openEmbedding_symm_target 📖	mathematical	Topology.IsOpenEmbedding	PartialEquiv.target toPartialEquiv symm lift_openEmbedding Set.image PartialEquiv.source	—	symm_target lift_openEmbedding_source
lift_openEmbedding_target 📖	mathematical	Topology.IsOpenEmbedding	PartialEquiv.target toPartialEquiv lift_openEmbedding	—	—
lift_openEmbedding_toFun 📖	mathematical	Topology.IsOpenEmbedding	toFun' lift_openEmbedding Function.extend Classical.arbitrary	—	—
lift_openEmbedding_trans 📖	mathematical	Topology.IsOpenEmbedding	trans symm lift_openEmbedding	—	ext lift_openEmbedding_trans_apply Function.Injective.extend_apply Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding Set.ext trans_source lift_openEmbedding_symm_source lift_openEmbedding_symm lift_openEmbedding_source Set.mem_preimage Set.mem_image_of_mem
lift_openEmbedding_trans_apply 📖	mathematical	Topology.IsOpenEmbedding	toFun' trans symm lift_openEmbedding	—	Function.Injective.extend_apply Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding
map_subtype_source 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	PartialEquiv.target instTopologicalSpaceSubtype subtypeRestr toFun'	—	map_source TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target Set.mem_preimage leftInvOn Subtype.prop
pi_apply 📖	mathematical	—	toFun' Pi.topologicalSpace pi	—	—
pi_source 📖	mathematical	—	PartialEquiv.source toPartialEquiv Pi.topologicalSpace pi Set.pi Set.univ	—	—
pi_symm_apply 📖	mathematical	—	toFun' Pi.topologicalSpace symm pi	—	—
pi_target 📖	mathematical	—	PartialEquiv.target toPartialEquiv Pi.topologicalSpace pi Set.pi Set.univ	—	—
pi_toPartialEquiv 📖	mathematical	—	toPartialEquiv Pi.topologicalSpace pi PartialEquiv.pi	—	—
piecewise_apply 📖	mathematical	IsImage Set Set.instInter PartialEquiv.source toPartialEquiv frontier Set.EqOn toFun'	piecewise Set.piecewise	—	—
piecewise_toPartialEquiv 📖	mathematical	IsImage Set Set.instInter PartialEquiv.source toPartialEquiv frontier Set.EqOn toFun'	piecewise PartialEquiv.piecewise	—	—
prod_apply 📖	mathematical	—	toFun' instTopologicalSpaceProd prod	—	—
prod_eq_prod_of_nonempty 📖	—	Set.Nonempty PartialEquiv.source toPartialEquiv instTopologicalSpaceProd prod	—	—	Set.prod_eq_prod_iff_of_nonempty
prod_eq_prod_of_nonempty' 📖	—	Set.Nonempty PartialEquiv.source toPartialEquiv instTopologicalSpaceProd prod	—	—	prod_eq_prod_of_nonempty
prod_source 📖	mathematical	—	PartialEquiv.source toPartialEquiv instTopologicalSpaceProd prod SProd.sprod Set Set.instSProd	—	—
prod_symm 📖	mathematical	—	symm instTopologicalSpaceProd prod	—	—
prod_symm_apply 📖	mathematical	—	toFun' instTopologicalSpaceProd symm prod	—	—
prod_symm_trans_prod 📖	mathematical	—	trans instTopologicalSpaceProd symm prod	—	prod_trans
prod_target 📖	mathematical	—	PartialEquiv.target toPartialEquiv instTopologicalSpaceProd prod SProd.sprod Set Set.instSProd	—	—
prod_toPartialEquiv 📖	mathematical	—	toPartialEquiv instTopologicalSpaceProd prod PartialEquiv.prod	—	—
prod_trans 📖	mathematical	—	trans instTopologicalSpaceProd prod	—	toPartialEquiv_injective PartialEquiv.prod_trans
refl_prod_refl 📖	mathematical	—	prod refl instTopologicalSpaceProd	—	ext Set.univ_prod_univ
subtypeRestr_coe 📖	mathematical	—	toFun' TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype subtypeRestr Set.restrict SetLike.coe	—	—
subtypeRestr_def 📖	mathematical	—	subtypeRestr trans TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe	—	—
subtypeRestr_source 📖	mathematical	—	PartialEquiv.source TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike toPartialEquiv instTopologicalSpaceSubtype subtypeRestr Set.preimage	—	Set.univ_inter
subtypeRestr_symm_apply 📖	mathematical	Set Set.instMembership PartialEquiv.target TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike toPartialEquiv instTopologicalSpaceSubtype subtypeRestr	toFun' symm	—	eq_symm_apply map_target subtypeRestr_source subtypeRestr_coe right_inv
subtypeRestr_symm_eqOn 📖	mathematical	—	Set.EqOn toFun' symm TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype subtypeRestr PartialEquiv.target toPartialEquiv	—	subtypeRestr_symm_apply
subtypeRestr_symm_eqOn_of_le 📖	mathematical	TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	Set.EqOn SetLike.instMembership TopologicalSpace.Opens.instSetLike toFun' instTopologicalSpaceSubtype symm subtypeRestr Set.Elem SetLike.coe Set.inclusion PartialEquiv.target toPartialEquiv	—	TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target injOn symm_target map_source symm_source right_inv
subtypeRestr_symm_trans_subtypeRestr 📖	mathematical	—	OpenPartialHomeomorph eqOnSourceSetoid trans TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype symm subtypeRestr restr Set Set.instInter PartialEquiv.target toPartialEquiv Set.preimage toFun' SetLike.coe	—	isOpen_inter_preimage_symm TopologicalSpace.Opens.is_open' ofSet_trans trans_assoc EqOnSource.trans' Set.ext ofSet_trans' trans_of_set' eqOnSource_refl open_target symm_trans_self TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target ofSet.congr_simp
subtypeRestr_target_subset 📖	mathematical	—	Set Set.instHasSubset PartialEquiv.target TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike toPartialEquiv instTopologicalSpaceSubtype subtypeRestr	—	image_source_eq_target subtypeRestr_source
symm_piecewise 📖	mathematical	IsImage Set Set.instInter PartialEquiv.source toPartialEquiv frontier Set.EqOn toFun'	symm piecewise IsImage.symm IsImage.inter_eq_of_inter_eq_of_eqOn IsImage.frontier IsImage.symm_eqOn_of_inter_eq_of_eqOn	—	—
transHomeomorph_apply 📖	mathematical	—	toFun' transHomeomorph DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	—
transHomeomorph_eq_trans 📖	mathematical	—	transHomeomorph trans Homeomorph.toOpenPartialHomeomorph	—	toPartialEquiv_injective PartialEquiv.transEquiv_eq_trans
transHomeomorph_source 📖	mathematical	—	PartialEquiv.source toPartialEquiv transHomeomorph	—	—
transHomeomorph_symm_apply 📖	mathematical	—	toFun' symm transHomeomorph DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm	—	—
transHomeomorph_target 📖	mathematical	—	PartialEquiv.target toPartialEquiv transHomeomorph Set.preimage DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm	—	—
transHomeomorph_transHomeomorph 📖	mathematical	—	transHomeomorph Homeomorph.trans	—	transHomeomorph_eq_trans trans_assoc Homeomorph.trans_toOpenPartialHomeomorph
trans_transHomeomorph 📖	mathematical	—	transHomeomorph trans	—	transHomeomorph_eq_trans trans_assoc

---

← Back to Index