feat: constructible sets

[YaelDillies]

Define constructible sets, which are morally sets in a topological space which we can make out of finite unions and intersections of open and closed sets.

From GrowthInGroups (LeanCamCombi)

---

[github-actions]

PR summary c2b4440b8d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Constructible (new file)	714

---

Declarations diff

+ IsConstructible
+ IsConstructible.biInter
+ IsConstructible.biUnion
+ IsConstructible.compl
+ IsConstructible.empty
+ IsConstructible.empty_union_induction
+ IsConstructible.himp
+ IsConstructible.iInter
+ IsConstructible.iUnion
+ IsConstructible.image_of_isClosedEmbedding
+ IsConstructible.image_of_isOpenEmbedding
+ IsConstructible.induction_of_isTopologicalBasis
+ IsConstructible.inter
+ IsConstructible.isLocallyConstructible
+ IsConstructible.of_compl
+ IsConstructible.preimage
+ IsConstructible.preimage_of_isClosedEmbedding
+ IsConstructible.preimage_of_isOpenEmbedding
+ IsConstructible.sInter
+ IsConstructible.sUnion
+ IsConstructible.sdiff
+ IsConstructible.union
+ IsConstructible.univ
+ IsLocallyConstructible
+ IsLocallyConstructible.empty
+ IsLocallyConstructible.finsetInf
+ IsLocallyConstructible.finsetInf'
+ IsLocallyConstructible.iInter
+ IsLocallyConstructible.inter
+ IsLocallyConstructible.sInter
+ IsLocallyConstructible.univ
+ IsRetrocompact
+ IsRetrocompact.biInter
+ IsRetrocompact.biUnion
+ IsRetrocompact.empty
+ IsRetrocompact.finsetInf
+ IsRetrocompact.finsetInf'
+ IsRetrocompact.finsetSup
+ IsRetrocompact.finsetSup'
+ IsRetrocompact.iInter
+ IsRetrocompact.iUnion
+ IsRetrocompact.image_of_isEmbedding
+ IsRetrocompact.inter
+ IsRetrocompact.inter_isOpen
+ IsRetrocompact.isOpen_inter
+ IsRetrocompact.preimage_of_isClosedEmbedding
+ IsRetrocompact.preimage_of_isOpenEmbedding
+ IsRetrocompact.sInter
+ IsRetrocompact.sUnion
+ IsRetrocompact.singleton
+ IsRetrocompact.union
+ IsRetrocompact.univ
+ IsRetrocompact_iff_isSpectralMap_subtypeVal
+ Topology.IsClosedEmbedding.inclusion
+ Topology.IsOpenEmbedding.inclusion
+ _root_.IsRetrocompact.isCompact
+ _root_.IsRetrocompact.isConstructible
+ _root_.IsRetrocompact.isLocallyConstructible
+ _root_.TopologicalSpace.IsTopologicalBasis.isConstructible
+ _root_.TopologicalSpace.IsTopologicalBasis.isConstructible'
+ _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact
+ _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact'
+ _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact
+ _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact'
+ isConstructible_compl
+ isConstructible_preimage_of_isOpenEmbedding

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).