mathlib

720aee9e - 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 <51336958+jlcbrown@users.noreply.github.com>