mathlib3
0fb6adae - chore(topology): move `exists_compact_superset`, drop assumption `t2_space` (#6327)

Commit

4 years ago

chore(topology): move `exists_compact_superset`, drop assumption `t2_space` (#6327) Also golf the proof of `is_compact.elim_finite_subcover_image`

Author

urkud

Parents