mathlib

c94a17c7 - feat(topology): a few simple lemmas (#11360)