Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 18:48 0fb6adae

View on Github →

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

Estimated changes

Modified src/topology/separation.lean

deleted theorem exists_compact_superset

Modified src/topology/subset_properties.lean

added theorem exists_compact_superset

added theorem finset.compact_bUnion