LocalAtTarget

📁 Source: Mathlib/Topology/LocalAtTarget.lean

Statistics

Metric	Count
Definitions	0
Theorems restrictPreimage, restrictPreimage, restrictPreimage, restrictPreimage, restrictPreimage_isClosedEmbedding, restrictPreimage_isEmbedding, restrictPreimage_isInducing, restrictPreimage_isOpenEmbedding, denseRange_iff_restrictPreimage, generalizingMap_iff_comp, generalizingMap_iff_restrictPreimage, isClosedEmbedding_iff_restrictPreimage, isClosedMap_iff_restrictPreimage, isClosed_iff_coe_preimage, isEmbedding_iff_restrictPreimage, isHomeomorph_iff_restrictPreimage, isInducing_iff_restrictPreimage, isLocallyClosed_iff_coe_preimage, isOpenEmbedding_iff_restrictPreimage, isOpenMap_iff_comp, isOpenMap_iff_restrictPreimage, isOpen_iff_coe_preimage, isOpen_iff_inter, restrictPreimage, restrictPreimage, restrictPreimage, restrictPreimage, isEmbedding_of_iSup_eq_top_of_preimage_subset_range	28
Total	28

GeneralizingMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	GeneralizingMap	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Specializes.map continuous_subtype_val Subtype.coe_eta

IsClosedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	IsClosedMap	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Set.image_restrictPreimage

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	IsOpenMap	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Set.image_restrictPreimage

IsProperMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	IsProperMap	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	isProperMap_iff_isClosedMap_and_compact_fibers Continuous.restrictPreimage continuous IsClosedMap.restrictPreimage isClosedMap Topology.IsEmbedding.isCompact_iff Topology.IsEmbedding.subtypeVal Set.image_val_preimage_restrictPreimage Set.image_singleton isCompact_preimage isCompact_singleton

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage_isClosedEmbedding 📖	mathematical	Topology.IsClosedEmbedding	Elem preimage instTopologicalSpaceSubtype Set instMembership restrictPreimage	—	Topology.IsEmbedding.restrictPreimage Topology.IsClosedEmbedding.toIsEmbedding Topology.IsInducing.isClosed_preimage Topology.IsInducing.subtypeVal Topology.IsClosedEmbedding.isClosed_range range_restrictPreimage
restrictPreimage_isEmbedding 📖	mathematical	Topology.IsEmbedding	Elem preimage instTopologicalSpaceSubtype Set instMembership restrictPreimage	—	Topology.IsInducing.restrictPreimage Topology.IsEmbedding.toIsInducing Function.Injective.restrictPreimage Topology.IsEmbedding.injective
restrictPreimage_isInducing 📖	mathematical	Topology.IsInducing	Elem preimage instTopologicalSpaceSubtype Set instMembership restrictPreimage	—	Topology.IsInducing.of_comp_iff Topology.IsInducing.subtypeVal mapsTo_preimage Filter.comap_comap Topology.IsInducing.nhds_eq_comap
restrictPreimage_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding	Elem preimage instTopologicalSpaceSubtype Set instMembership restrictPreimage	—	Topology.IsEmbedding.restrictPreimage Topology.IsOpenEmbedding.toIsEmbedding Continuous.isOpen_preimage continuous_subtype_val Topology.IsOpenEmbedding.isOpen_range range_restrictPreimage

TopologicalSpace.IsOpenCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denseRange_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover	DenseRange Set.Elem TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.preimage Set.restrictPreimage	—	Set.range_restrictPreimage IsOpenMap.preimage_closure_eq_closure_preimage Topology.IsOpenEmbedding.isOpenMap IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.is_open' continuous_subtype_val Subtype.range_coe_subtype Set.iUnion_subset_iff Set.univ_subset_iff iSup_set_eq_univ
generalizingMap_iff_comp 📖	mathematical	TopologicalSpace.IsOpenCover	GeneralizingMap TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype	—	GeneralizingMap.comp Topology.IsInducing.generalizingMap Topology.IsEmbedding.toIsInducing Topology.IsOpenEmbedding.toIsEmbedding TopologicalSpace.Opens.isOpenEmbedding' IsOpen.stableUnderGeneralization Topology.IsOpenEmbedding.isOpen_range exists_mem Specializes.map Topology.IsOpenEmbedding.continuous
generalizingMap_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover	GeneralizingMap Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	GeneralizingMap.restrictPreimage exists_mem IsOpen.stableUnderGeneralization TopologicalSpace.Opens.is_open' subtype_specializes_iff
isClosedEmbedding_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover Continuous	Topology.IsClosedEmbedding Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	isEmbedding_iff_restrictPreimage Set.range_restrictPreimage isClosed_iff_coe_preimage
isClosedMap_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover	IsClosedMap Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	IsClosedMap.restrictPreimage isClosed_iff_coe_preimage Set.ext Set.image_congr compl_compl IsClosed.isOpen_compl eq_compl_comm
isClosed_iff_coe_preimage 📖	mathematical	TopologicalSpace.IsOpenCover	IsClosed TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype Set.preimage	—	isOpen_iff_coe_preimage
isEmbedding_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover Continuous	Topology.IsEmbedding Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	isInducing_iff_restrictPreimage Set.injective_iff_injective_of_iUnion_eq_univ iSup_set_eq_univ
isHomeomorph_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover Continuous	IsHomeomorph Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	isEmbedding_iff_restrictPreimage Set.surjective_iff_surjective_of_iUnion_eq_univ iSup_set_eq_univ
isInducing_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover Continuous	Topology.IsInducing Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Topology.IsInducing.of_comp_iff Topology.IsInducing.subtypeVal Set.mapsTo_preimage Topology.IsInducing.nhds_eq_comap TopologicalSpace.Opens.mem_iSup iSup_eq_top Topology.IsOpenEmbedding.map_nhds_eq IsOpen.isOpenEmbedding_subtypeVal Continuous.isOpen_preimage TopologicalSpace.Opens.is_open' Filter.subtype_coe_map_comap Filter.preimage_mem_comap IsOpen.mem_nhds
isLocallyClosed_iff_coe_preimage 📖	mathematical	TopologicalSpace.IsOpenCover	IsLocallyClosed TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype Set.preimage	—	Topology.IsOpenEmbedding.coborder_preimage IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.isOpen isOpen_iff_coe_preimage
isOpenEmbedding_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover Continuous	Topology.IsOpenEmbedding Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	isEmbedding_iff_restrictPreimage Set.range_restrictPreimage isOpen_iff_coe_preimage
isOpenMap_iff_comp 📖	mathematical	TopologicalSpace.IsOpenCover	IsOpenMap TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype	—	IsOpenMap.comp Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.isOpenEmbedding' Set.image_comp Set.image_preimage_eq_inter_range Subtype.range_coe_subtype iUnion_inter isOpen_iUnion isOpen_induced
isOpenMap_iff_restrictPreimage 📖	mathematical	TopologicalSpace.IsOpenCover	IsOpenMap Set.Elem Set.preimage TopologicalSpace.Opens.carrier instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	IsOpenMap.restrictPreimage isOpen_iff_coe_preimage Set.ext Set.image_congr IsOpen.preimage continuous_subtype_val
isOpen_iff_coe_preimage 📖	mathematical	TopologicalSpace.IsOpenCover	IsOpen TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype Set.preimage	—	isOpen_iff_inter Topology.IsOpenEmbedding.isOpen_iff_image_isOpen IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.is_open' Set.image_congr Set.image_preimage_eq_inter_range Subtype.range_coe_subtype
isOpen_iff_inter 📖	mathematical	TopologicalSpace.IsOpenCover	IsOpen Set Set.instInter SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	IsOpen.inter TopologicalSpace.Opens.isOpen iSup_set_eq_univ Set.inter_univ isOpen_iUnion

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	Topology.IsClosedEmbedding	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Set.restrictPreimage_isClosedEmbedding

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	Topology.IsEmbedding	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Set.restrictPreimage_isEmbedding

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	Topology.IsInducing	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Set.restrictPreimage_isInducing

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage 📖	mathematical	Topology.IsOpenEmbedding	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Set.restrictPreimage_isOpenEmbedding

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmbedding_of_iSup_eq_top_of_preimage_subset_range 📖	—	Continuous Set Set.instHasSubset Set.range SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice Set.preimage Topology.IsEmbedding	—	—	TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage Topology.IsEmbedding.comp Topology.IsEmbedding.subtypeVal Topology.IsEmbedding.restrictPreimage Topology.IsEmbedding.of_comp Set.range_comp Set.range_restrictPreimage Subtype.image_preimage_coe Continuous.restrictPreimage continuous_subtype_val Homeomorph.surjective Homeomorph.symm_apply_apply Homeomorph.isEmbedding top_le_iff isOpen_iUnion TopologicalSpace.Opens.is_open' instIsConcreteLE TopologicalSpace.Opens.coe_iSup Continuous.comp'

---

← Back to Index