Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 08:37 5a3abca1

View on Github →

feat(topology/subset_properties): some compactness properties (#11425)

Add some lemmas about the existence of compact sets
Add is_compact.eventually_forall_of_forall_eventually
Some cleanup in topology/subset_properties and topology/separation

Estimated changes

Modified src/topology/separation.lean

added theorem exists_compact_between

added theorem exists_open_between_and_is_compact_closure

added theorem exists_open_superset_and_is_compact_closure

Modified src/topology/subset_properties.lean

modified theorem compact_Union

modified theorem compact_space.elim_nhds_subcover

modified theorem compact_space_of_finite_subfamily_closed

modified theorem continuous_on.preimage_clopen_of_clopen

modified theorem finset.compact_bUnion

modified theorem is_clopen_bInter

modified theorem is_clopen_bUnion

modified theorem is_compact.elim_finite_subcover_image

added theorem is_compact.eventually_forall_of_forall_eventually

modified def is_compact

modified theorem is_irreducible.image

modified theorem is_preirreducible.image

modified theorem is_preirreducible.preimage

modified theorem set.finite.compact_bUnion