feat(topology/subset_properties): Add `is_clopen.preimage` (#17469)
feat(topology/subset_properties): Add `is_clopen.preimage` (#17469)

Adds a lemma proving the pre-image of a clopen set under a continuous map is clopen.



Co-authored-by: jlcbrown <b33fe64c79f00f9b3e62c7f13f3a592e1973bba2@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib