mathlib

5558fd9f - feat(topology/subset_properties): open/closed sets are locally compact spaces (#10844)

feat(topology/subset_properties): open/closed sets are locally compact spaces (#10844) * add `inducing.image_mem_nhds_within`; * move `inducing.is_compact_iff` up, use it to prove `embedding.is_compact_iff_is_compact_image`; * prove `closed_embedding.is_compact_preimage`, use it to prove `closed_embedding.tendsto_cocompact`; * prove `closed_embedding.locally_compact_space`, `open_embedding.locally_compact_space`; * specialize to `is_closed.locally_compact_space`, `is_open.locally_compact_space`; * rename `locally_finite.countable_of_sigma_compact` to `locally_finite.countable_univ`, provide `locally_finite.encodable`.