Commit 2023-07-31 08:03 accdefb0

View on Github →

feat(Topology.ProperMap): basic theory of proper maps (#6005)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Prod.lean

added theorem Filter.le_prod

Modified Mathlib/Topology/Basic.lean

added theorem clusterPt_iff_forall_mem_closure

added theorem clusterPt_iff_lift'_closure'

added theorem clusterPt_iff_lift'_closure

added theorem clusterPt_lift'_closure_iff

Modified Mathlib/Topology/Filter.lean

Modified Mathlib/Topology/Maps.lean

added theorem IsClosedMap.closure_image_eq_of_continuous

added theorem IsClosedMap.lift'_closure_map_eq

added theorem IsClosedMap.mapClusterPt_iff_lift'_closure

Created Mathlib/Topology/ProperMap.lean

added theorem Homeomorph.isProperMap

added theorem IsProperMap.continuous

added theorem IsProperMap.isClosedMap

added theorem IsProperMap.isCompact_preimage

added theorem IsProperMap.pi_map

added theorem IsProperMap.prod_map

added theorem IsProperMap.ultrafilter_le_nhds_of_tendsto

added theorem IsProperMap.universally_closed

added structure IsProperMap

added theorem isProperMap_id

added theorem isProperMap_iff_isClosedMap_and_compact_fibers

added theorem isProperMap_iff_isClosedMap_and_tendsto_cofinite

added theorem isProperMap_iff_isClosedMap_filter

added theorem isProperMap_iff_isClosedMap_ultrafilter

added theorem isProperMap_iff_isCompact_preimage

added theorem isProperMap_iff_tendsto_cocompact

added theorem isProperMap_iff_ultrafilter

added theorem isProperMap_iff_universally_closed

Modified Mathlib/Topology/StoneCech.lean

added theorem Ultrafilter.tendsto_pure_self