Commit 2024-03-30 17:04 345188e4

View on Github →

feat: new lemmas about proper maps in Mathlib.Topology.ProperMap (#11754) These are new lemmas added to the file about proper maps.

Estimated changes

Modified Mathlib/Topology/Basic.lean

added theorem mapClusterPt_comp

Modified Mathlib/Topology/ProperMap.lean

modified theorem Homeomorph.isProperMap

added theorem IsProperMap.closed_range

added theorem IsProperMap.comp

added theorem isProperMap_iff_isClosedMap_of_inj

added theorem isProperMap_of_closedEmbedding

added theorem isProperMap_of_comp_of_inj

added theorem isProperMap_of_comp_of_surj

added theorem isProperMap_of_comp_of_t2

added theorem isProperMap_of_isClosedMap_of_inj

added theorem isProperMap_restr_of_proper_of_closed

added theorem isProperMap_subtype_val_of_closed