Lemmas

📁 Source: Mathlib/Topology/Homeomorph/Lemmas.lean

Statistics

Metric	Count
Definitions `homeoOfEquivCompactToT2`, `appendHomeomorph`, `prod`, `univ`, `finTwoArrow`, `funSplitAt`, `funUnique`, `image`, `ofDiscrete`, `piCongr`, `piCongrLeft`, `piCongrRight`, `piEquivPiSubtypeProd`, `piFinTwo`, `piSplitAt`, `piUnique`, `prodUnique`, `setCongr`, `sets`, `sigmaProdDistrib`, `subtype`, `sumArrowHomeomorphProdArrow`, `sumPiEquivProdPi`, `ulift`, `uniqueProd`, `homeomorph`, `homeomorphImage`, `homeomorphOfSubsetRange`, `toHomeomorph`, `toHomeomorphOfSurjective`	30
Theorems `continuous_symm_of_equiv_compact_to_t2`, `toEquiv_homeoOfEquivCompactToT2`, `isHomeomorph_of_discrete`, `appendHomeomorph_apply`, `appendHomeomorph_symm_apply`, `appendHomeomorph_toEquiv`, `continuous_append`, `prod_apply`, `prod_symm_apply_coe`, `univ_apply`, `univ_symm_apply_coe`, `baireSpace`, `coe_prodUnique`, `coe_uniqueProd`, `comap_coclosedCompact`, `comap_cocompact`, `comp_continuousOn_iff`, `comp_continuousWithinAt_iff`, `compactSpace`, `finTwoArrow_apply`, `finTwoArrow_symm_apply`, `funSplitAt_apply`, `funSplitAt_symm_apply`, `funUnique_apply`, `funUnique_symm_apply`, `image_apply_coe`, `image_connectedComponentIn`, `image_symm_apply_coe`, `isCompact_image`, `isCompact_preimage`, `isConnected_image`, `isConnected_preimage`, `isDenseEmbedding`, `isPreconnected_image`, `isPreconnected_preimage`, `isSigmaCompact_image`, `isSigmaCompact_preimage`, `locallyCompactSpace_iff`, `locallyConnectedSpace`, `map_coclosedCompact`, `map_cocompact`, `map_punctured_nhds_eq`, `piCongrLeft_apply`, `piCongrLeft_apply_apply`, `piCongrLeft_refl`, `piCongrLeft_symm_apply`, `piCongrRight_apply`, `piCongrRight_symm`, `piCongr_apply`, `piEquivPiSubtypeProd_apply`, `piEquivPiSubtypeProd_symm_apply`, `piFinTwo_apply`, `piFinTwo_symm_apply`, `piSplitAt_apply`, `piSplitAt_symm_apply`, `piUnique_apply`, `piUnique_symm_apply`, `prodUnique_symm_apply_snd`, `secondCountableTopology`, `sigmaProdDistrib_apply`, `sigmaProdDistrib_symm_apply`, `subtype_apply_coe`, `subtype_symm_apply_coe`, `subtype_toEquiv`, `sumArrowHomeomorphProdArrow_apply`, `sumArrowHomeomorphProdArrow_symm_apply`, `toEquiv_piCongr`, `toEquiv_piCongrLeft`, `toEquiv_piCongrRight`, `toEquiv_sigmaProdDistrib`, `totallyDisconnectedSpace`, `uniqueProd_symm_apply_snd`, `homeomorph_apply`, `homeomorph_symm_apply`, `isClosedEmbedding`, `isClosedMap`, `isDenseEmbedding`, `isEmbedding`, `isInducing`, `isOpenEmbedding`, `isQuotientMap`, `pi_map`, `prodMap`, `sigmaMap`, `sumMap`, `toEquiv_homeomorph`, `uliftMap`, `homeomorphOfSubsetRange_apply_coe`, `toHomeomorphOfSurjective_apply`, `toHomeomorph_apply_coe`, `toHomeomorph_symm_apply`, `uliftMap`, `uliftMap`, `isHomeomorph_iff_continuous_bijective`, `isHomeomorph_iff_continuous_isClosedMap_bijective`, `isHomeomorph_iff_exists_homeomorph`, `isHomeomorph_iff_exists_inverse`, `isHomeomorph_iff_isEmbedding_surjective`	98
Total	128

Continuous

Definitions

Name	Category	Theorems
`homeoOfEquivCompactToT2` 📖	CompOp	1 math math: `toEquiv_homeoOfEquivCompactToT2`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_symm_of_equiv_compact_to_t2` 📖	mathematical	`Continuous` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv.symm`	—	`continuous_iff_isClosed` `IsCompact.isClosed` `IsCompact.image` `IsClosed.isCompact` `Equiv.image_eq_preimage_symm`
`toEquiv_homeoOfEquivCompactToT2` 📖	mathematical	`Continuous` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Homeomorph.toEquiv` `homeoOfEquivCompactToT2`	—	—

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHomeomorph_of_discrete` 📖	mathematical	—	`IsHomeomorph` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`Homeomorph.isHomeomorph`

Fin

Definitions

Name	Category	Theorems
`appendHomeomorph` 📖	CompOp	4 math math: `appendHomeomorph_apply`, `appendIsometry_toHomeomorph`, `appendHomeomorph_toEquiv`, `appendHomeomorph_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`appendHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `appendHomeomorph` `append`	—	—
`appendHomeomorph_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `appendHomeomorph`	—	—
`appendHomeomorph_toEquiv` 📖	mathematical	—	`Homeomorph.toEquiv` `instTopologicalSpaceProd` `Pi.topologicalSpace` `appendHomeomorph` `appendEquiv`	—	—
`continuous_append` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `Pi.topologicalSpace` `append`	—	`Homeomorph.continuous_toFun`

Homeomorph

Definitions

Name	Category	Theorems
`finTwoArrow` 📖	CompOp	2 math math: `finTwoArrow_apply`, `finTwoArrow_symm_apply`
`funSplitAt` 📖	CompOp	2 math math: `funSplitAt_symm_apply`, `funSplitAt_apply`
`funUnique` 📖	CompOp	2 math math: `funUnique_apply`, `funUnique_symm_apply`
`image` 📖	CompOp	2 math math: `image_apply_coe`, `image_symm_apply_coe`
`ofDiscrete` 📖	CompOp	—
`piCongr` 📖	CompOp	2 math math: `piCongr_apply`, `toEquiv_piCongr`
`piCongrLeft` 📖	CompOp	5 math math: `piCongrLeft_symm_apply`, `toEquiv_piCongrLeft`, `piCongrLeft_apply_apply`, `piCongrLeft_apply`, `piCongrLeft_refl`
`piCongrRight` 📖	CompOp	3 math math: `toEquiv_piCongrRight`, `piCongrRight_apply`, `piCongrRight_symm`
`piEquivPiSubtypeProd` 📖	CompOp	2 math math: `piEquivPiSubtypeProd_apply`, `piEquivPiSubtypeProd_symm_apply`
`piFinTwo` 📖	CompOp	2 math math: `piFinTwo_apply`, `piFinTwo_symm_apply`
`piSplitAt` 📖	CompOp	2 math math: `piSplitAt_symm_apply`, `piSplitAt_apply`
`piUnique` 📖	CompOp	2 math math: `piUnique_apply`, `piUnique_symm_apply`
`prodUnique` 📖	CompOp	3 math math: `prodUnique_symm_apply_snd`, `uniqueProd_symm_apply_snd`, `coe_prodUnique`
`setCongr` 📖	CompOp	—
`sets` 📖	CompOp	—
`sigmaProdDistrib` 📖	CompOp	3 math math: `sigmaProdDistrib_symm_apply`, `toEquiv_sigmaProdDistrib`, `sigmaProdDistrib_apply`
`subtype` 📖	CompOp	3 math math: `subtype_symm_apply_coe`, `subtype_toEquiv`, `subtype_apply_coe`
`sumArrowHomeomorphProdArrow` 📖	CompOp	3 math math: `IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph`, `sumArrowHomeomorphProdArrow_apply`, `sumArrowHomeomorphProdArrow_symm_apply`
`sumPiEquivProdPi` 📖	CompOp	—
`ulift` 📖	CompOp	—
`uniqueProd` 📖	CompOp	2 math math: `coe_uniqueProd`, `uniqueProd_symm_apply_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baireSpace` 📖	mathematical	—	`BaireSpace`	—	`IsOpenQuotientMap.baireSpace` `isOpenQuotientMap`
`coe_prodUnique` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `prodUnique`	—	—
`coe_uniqueProd` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `uniqueProd`	—	—
`comap_coclosedCompact` 📖	mathematical	—	`Filter.comap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `Filter.coclosedCompact`	—	`Filter.HasBasis.eq_of_same_basis` `Filter.HasBasis.comap` `Filter.hasBasis_coclosedCompact` `Filter.HasBasis.comp_surjective` `Function.Injective.preimage_surjective` `injective`
`comap_cocompact` 📖	mathematical	—	`Filter.comap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `Filter.cocompact`	—	`LE.le.antisymm` `Filter.comap_cocompact_le` `continuous` `Filter.HasBasis.le_basis_iff` `Filter.hasBasis_cocompact` `Filter.HasBasis.comap` `isCompact_preimage` `Set.Subset.rfl`
`comp_continuousOn_iff` 📖	mathematical	—	`ContinuousOn` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Topology.IsInducing.continuousOn_iff` `isInducing`
`comp_continuousWithinAt_iff` 📖	mathematical	—	`ContinuousWithinAt` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Topology.IsInducing.continuousWithinAt_iff` `isInducing`
`compactSpace` 📖	mathematical	—	`CompactSpace`	—	`isCompact_preimage` `isCompact_univ`
`finTwoArrow_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `finTwoArrow`	—	—
`finTwoArrow_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `finTwoArrow` `Matrix.vecCons` `Matrix.vecEmpty`	—	—
`funSplitAt_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `funSplitAt`	—	—
`funSplitAt_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `funSplitAt`	—	—
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `funUnique` `Unique.instInhabited`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `funUnique` `uniqueElim`	—	—
`image_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `Homeomorph` `Set.Elem` `instEquivLike` `instTopologicalSpaceSubtype` `image`	—	—
`image_connectedComponentIn` 📖	mathematical	`Set` `Set.instMembership`	`Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `connectedComponentIn`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Continuous.image_connectedComponentIn_subset` `continuous` `Set.mem_image_of_mem` `symm_apply_apply` `preimage_image` `image_symm` `preimage_symm` `Set.image_subset_iff`
`image_symm_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `DFunLike.coe` `Homeomorph` `Set.Elem` `Set.image` `EquivLike.toFunLike` `instEquivLike` `instTopologicalSpaceSubtype` `symm` `image`	—	—
`isCompact_image` 📖	mathematical	—	`IsCompact` `Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Topology.IsEmbedding.isCompact_iff` `isEmbedding`
`isCompact_preimage` 📖	mathematical	—	`IsCompact` `Set.preimage` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `isCompact_image`
`isConnected_image` 📖	mathematical	—	`IsConnected` `Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Iff.and` `Set.image_nonempty` `isPreconnected_image`
`isConnected_preimage` 📖	mathematical	—	`IsConnected` `Set.preimage` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `isConnected_image`
`isDenseEmbedding` 📖	mathematical	—	`IsDenseEmbedding` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`isEmbedding` `Topology.IsEmbedding.toIsInducing` `Function.Surjective.denseRange` `surjective` `Topology.IsEmbedding.injective`
`isPreconnected_image` 📖	mathematical	—	`IsPreconnected` `Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `preimage_image` `IsPreconnected.image` `Continuous.continuousOn` `continuous`
`isPreconnected_preimage` 📖	mathematical	—	`IsPreconnected` `Set.preimage` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `isPreconnected_image`
`isSigmaCompact_image` 📖	mathematical	—	`IsSigmaCompact` `Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Topology.IsEmbedding.isSigmaCompact_iff` `isEmbedding`
`isSigmaCompact_preimage` 📖	mathematical	—	`IsSigmaCompact` `Set.preimage` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `isSigmaCompact_image`
`locallyCompactSpace_iff` 📖	mathematical	—	`LocallyCompactSpace`	—	`Topology.IsOpenEmbedding.locallyCompactSpace` `isOpenEmbedding` `Topology.IsClosedEmbedding.locallyCompactSpace` `isClosedEmbedding`
`locallyConnectedSpace` 📖	mathematical	—	`LocallyConnectedSpace`	—	`symm_map_nhds_eq` `Filter.HasBasis.map` `LocallyConnectedSpace.open_connected_basis` `locallyConnectedSpace_of_connected_bases` `IsPreconnected.image` `Continuous.continuousOn` `continuous`
`map_coclosedCompact` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `Filter.coclosedCompact`	—	`comap_coclosedCompact` `Filter.map_comap_of_surjective` `surjective`
`map_cocompact` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `Filter.cocompact`	—	`comap_cocompact` `Filter.map_comap_of_surjective` `surjective`
`map_punctured_nhds_eq` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`image_compl` `Set.image_singleton` `Topology.IsEmbedding.map_nhdsWithin_eq` `isEmbedding`
`piCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft` `Equiv.symm` `Equiv.piCongrLeft'`	—	—
`piCongrLeft_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `piCongrLeft`	—	`Equiv.piCongrLeft_apply_apply`
`piCongrLeft_refl` 📖	mathematical	—	`piCongrLeft` `Equiv.refl` `refl` `Pi.topologicalSpace`	—	—
`piCongrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instEquivLike` `symm` `piCongrLeft`	—	—
`piCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `piCongrRight`	—	—
`piCongrRight_symm` 📖	mathematical	—	`symm` `Pi.topologicalSpace` `piCongrRight`	—	—
`piCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `piCongr` `Equiv` `Equiv.instEquivLike` `Equiv.piCongrLeft` `Equiv.piCongrRight` `toEquiv`	—	—
`piEquivPiSubtypeProd_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `piEquivPiSubtypeProd`	—	—
`piEquivPiSubtypeProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `piEquivPiSubtypeProd`	—	—
`piFinTwo_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `piFinTwo`	—	—
`piFinTwo_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `piFinTwo` `Fin.cons` `finZeroElim`	—	—
`piSplitAt_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `piSplitAt`	—	—
`piSplitAt_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `piSplitAt`	—	—
`piUnique_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Unique.instInhabited` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `piUnique`	—	—
`piUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Unique.instInhabited` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `piUnique` `uniqueElim`	—	—
`prodUnique_symm_apply_snd` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `symm` `prodUnique` `Unique.instInhabited`	—	—
`secondCountableTopology` 📖	mathematical	—	`SecondCountableTopology`	—	`Topology.IsInducing.secondCountableTopology` `isInducing`
`sigmaProdDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `instTopologicalSpaceSigma` `EquivLike.toFunLike` `instEquivLike` `sigmaProdDistrib`	—	—
`sigmaProdDistrib_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceSigma` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `symm` `sigmaProdDistrib`	—	—
`subtype_apply_coe` 📖	mathematical	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	`instTopologicalSpaceSubtype` `subtype`	—	—
`subtype_symm_apply_coe` 📖	mathematical	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	`instTopologicalSpaceSubtype` `symm` `subtype`	—	—
`subtype_toEquiv` 📖	mathematical	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	`toEquiv` `instTopologicalSpaceSubtype` `subtype` `Equiv.subtypeEquiv`	—	—
`sumArrowHomeomorphProdArrow_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Pi.topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `sumArrowHomeomorphProdArrow`	—	—
`sumArrowHomeomorphProdArrow_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `Pi.topologicalSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `sumArrowHomeomorphProdArrow`	—	—
`toEquiv_piCongr` 📖	mathematical	—	`toEquiv` `Pi.topologicalSpace` `piCongr` `Equiv.trans` `Equiv.piCongrRight` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piCongrLeft`	—	—
`toEquiv_piCongrLeft` 📖	mathematical	—	`toEquiv` `Pi.topologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `piCongrLeft` `Equiv.piCongrLeft`	—	—
`toEquiv_piCongrRight` 📖	mathematical	—	`toEquiv` `Pi.topologicalSpace` `piCongrRight` `Equiv.piCongrRight`	—	—
`toEquiv_sigmaProdDistrib` 📖	mathematical	—	`toEquiv` `instTopologicalSpaceProd` `instTopologicalSpaceSigma` `sigmaProdDistrib` `Equiv.sigmaProdDistrib`	—	—
`totallyDisconnectedSpace` 📖	mathematical	—	`TotallyDisconnectedSpace`	—	`totallyDisconnectedSpace_iff` `Topology.IsEmbedding.isTotallyDisconnected_range` `isEmbedding` `range_coe`
`uniqueProd_symm_apply_snd` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `EquivLike.toFunLike` `instEquivLike` `symm` `uniqueProd` `prodUnique`	—	—

Homeomorph.Set

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	2 math math: `prod_apply`, `prod_symm_apply_coe`
`univ` 📖	CompOp	2 math math: `univ_symm_apply_coe`, `univ_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd` `instTopologicalSpaceSubtype` `Set.instMembership` `instTopologicalSpaceProd` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `prod`	—	—
`prod_symm_apply_coe` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set.instMembership` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `prod`	—	—
`univ_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Set.Elem` `Set.univ` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `univ`	—	—
`univ_symm_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Set.univ` `DFunLike.coe` `Homeomorph` `Set.Elem` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `univ`	—	—

IsHomeomorph

Definitions

Name	Category	Theorems
`homeomorph` 📖	CompOp	3 math math: `homeomorph_symm_apply`, `toEquiv_homeomorph`, `homeomorph_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homeomorph_apply` 📖	mathematical	`IsHomeomorph`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorph`	—	—
`homeomorph_symm_apply` 📖	mathematical	`IsHomeomorph`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorph` `Function.surjInv` `Function.Bijective.surjective` `bijective`	—	—
`isClosedEmbedding` 📖	mathematical	`IsHomeomorph`	`Topology.IsClosedEmbedding`	—	`Homeomorph.isClosedEmbedding`
`isClosedMap` 📖	mathematical	`IsHomeomorph`	`IsClosedMap`	—	`Homeomorph.isClosedMap`
`isDenseEmbedding` 📖	mathematical	`IsHomeomorph`	`IsDenseEmbedding`	—	`Homeomorph.isDenseEmbedding`
`isEmbedding` 📖	mathematical	`IsHomeomorph`	`Topology.IsEmbedding`	—	`Homeomorph.isEmbedding`
`isInducing` 📖	mathematical	`IsHomeomorph`	`Topology.IsInducing`	—	`Homeomorph.isInducing`
`isOpenEmbedding` 📖	mathematical	`IsHomeomorph`	`Topology.IsOpenEmbedding`	—	`Homeomorph.isOpenEmbedding`
`isQuotientMap` 📖	mathematical	`IsHomeomorph`	`Topology.IsQuotientMap`	—	`Homeomorph.isQuotientMap`
`pi_map` 📖	mathematical	`IsHomeomorph`	`Pi.topologicalSpace`	—	`Homeomorph.isHomeomorph`
`prodMap` 📖	mathematical	`IsHomeomorph`	`instTopologicalSpaceProd`	—	`Continuous.prodMap` `continuous` `IsOpenMap.prodMap` `isOpenMap` `Function.Bijective.prodMap` `bijective`
`sigmaMap` 📖	mathematical	`Function.Bijective` `IsHomeomorph`	`instTopologicalSpaceSigma` `Sigma.map`	—	`Topology.isEmbedding_sigmaMap` `Function.Surjective.sigma_map`
`sumMap` 📖	mathematical	`IsHomeomorph`	`instTopologicalSpaceSum`	—	`Continuous.sumMap` `continuous` `IsOpenMap.sumMap` `isOpenMap` `Function.Bijective.sumMap` `bijective`
`toEquiv_homeomorph` 📖	mathematical	`IsHomeomorph`	`Homeomorph.toEquiv` `homeomorph` `Equiv.ofBijective` `bijective`	—	—

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uliftMap` 📖	mathematical	`Topology.IsClosedEmbedding`	`ULift.topologicalSpace` `ULift.map`	—	`comp` `Homeomorph.isClosedEmbedding`

Topology.IsEmbedding

Definitions

Name	Category	Theorems
`homeomorphImage` 📖	CompOp	—
`homeomorphOfSubsetRange` 📖	CompOp	1 math math: `homeomorphOfSubsetRange_apply_coe`
`toHomeomorph` 📖	CompOp	2 math math: `toHomeomorph_apply_coe`, `toHomeomorph_symm_apply`
`toHomeomorphOfSurjective` 📖	CompOp	1 math math: `toHomeomorphOfSurjective_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homeomorphOfSubsetRange_apply_coe` 📖	mathematical	`Topology.IsEmbedding` `Set` `Set.instHasSubset` `Set.range`	`Set.instMembership` `DFunLike.coe` `Homeomorph` `Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphOfSubsetRange`	—	—
`toHomeomorphOfSurjective_apply` 📖	mathematical	`Topology.IsEmbedding`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorphOfSurjective`	—	—
`toHomeomorph_apply_coe` 📖	mathematical	`Topology.IsEmbedding`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Homeomorph` `Set.Elem` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorph`	—	—
`toHomeomorph_symm_apply` 📖	mathematical	`Topology.IsEmbedding`	`DFunLike.coe` `Homeomorph` `Set.Elem` `Set.range` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorph`	—	`Homeomorph.injective` `Homeomorph.apply_symm_apply`
`uliftMap` 📖	mathematical	`Topology.IsEmbedding`	`ULift.topologicalSpace` `ULift.map`	—	`comp` `Homeomorph.isEmbedding`

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uliftMap` 📖	mathematical	`Topology.IsOpenEmbedding`	`ULift.topologicalSpace` `ULift.map`	—	`comp` `Homeomorph.isOpenEmbedding`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHomeomorph_iff_continuous_bijective` 📖	mathematical	—	`IsHomeomorph` `Continuous` `Function.Bijective`	—	`isHomeomorph_iff_continuous_isClosedMap_bijective` `Continuous.isClosedMap`
`isHomeomorph_iff_continuous_isClosedMap_bijective` 📖	mathematical	—	`IsHomeomorph` `Continuous` `IsClosedMap` `Function.Bijective`	—	`IsHomeomorph.continuous` `IsHomeomorph.isClosedMap` `IsHomeomorph.bijective` `isClosed_compl_iff` `IsOpen.isClosed_compl` `Set.image_compl_eq`
`isHomeomorph_iff_exists_homeomorph` 📖	mathematical	—	`IsHomeomorph` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.isHomeomorph`
`isHomeomorph_iff_exists_inverse` 📖	mathematical	—	`IsHomeomorph` `Continuous`	—	`IsHomeomorph.continuous` `Equiv.left_inv` `Equiv.right_inv` `Homeomorph.continuous_invFun` `Homeomorph.isHomeomorph`
`isHomeomorph_iff_isEmbedding_surjective` 📖	mathematical	—	`IsHomeomorph` `Topology.IsEmbedding`	—	`IsHomeomorph.isEmbedding` `IsHomeomorph.surjective` `Topology.IsEmbedding.continuous` `Topology.IsOpenEmbedding.isOpenMap` `Topology.isOpenEmbedding_iff` `isOpen_univ` `Function.Surjective.range_eq` `Topology.IsEmbedding.injective`

---

← Back to Index