Commit 2023-08-30 16:50 bae4f344

View on Github →

feat: define ProperConstSMul (#6675)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/ProperConstSMul.lean

added theorem IsCompact.preimage_smul

added theorem isProperMap_smul

Modified Mathlib/Topology/ProperMap.lean

added theorem Continuous.isProperMap

added theorem isProperMap_iff_ultrafilter_of_t2

Modified Mathlib/Topology/Separation.lean

added theorem IsCompact.preimage_continuous