mathlib

c28dc84a - feat(topology/subset_properties): more facts about compact sets (#11939)

feat(topology/subset_properties): more facts about compact sets (#11939) * add `tendsto.is_compact_insert_range_of_cocompact`, `tendsto.is_compact_insert_range_of_cofinite`, and `tendsto.is_compact_insert_range`; * reuse the former in `alexandroff.compact_space`; * rename `finite_of_is_compact_of_discrete` to `is_compact.finite_of_discrete`, add `is_compact_iff_finite`; * add `cocompact_le_cofinite`, `cocompact_eq_cofinite`; * add `int.cofinite_eq`, add `@[simp]` to `nat.cofinite_eq`; * add `set.insert_none_range_some`; * move `is_compact.image_of_continuous_on` and `is_compact_image` up;