mathlib

048263d9 - feat(topology/basic): add two lemmas about frontier and two lemmas about preimages under continuous maps (#8329)

feat(topology/basic): add two lemmas about frontier and two lemmas about preimages under continuous maps (#8329) Adding four lemmas: `frontier_eq_inter_compl_interior`, `compl_frontier_eq_union_interior`, `continuous.closure_preimage_subset`, `continuous.frontier_preimage_subset` to `topology/basic`. These were discussed on Zulip <https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Portmanteau.20theorem/near/246037950>. The formulations closely follow Patrick's suggestions. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>