mathlib3

feat(topology): is_closed_proj_of_compact

#2069

Merged