Commit 2022-02-10 18:46 c28dc84a

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;