feat(Topology): étalé space associated to a predicate on sections

[alreadydone]

---

migrated from #22782

[github-actions]

PR summary 82d756ea35

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ EtaleSpace
+ HasIdentityPrinciple
+ HasIdentityPrinciple.isSeparated
+ HasIdentityPrinciple.isStalkInj
+ HasIdentityPrincipleOn
+ IsConstantOn
+ IsConstantOn.hasIdentityPrincipleOn
+ IsLocal
+ IsLocal.inf
+ IsLocalHomeomorph.isSeparated_of_isSeparatedMap
+ IsLocalHomeomorph.isStalkSurj
+ IsLocallyConstant
+ IsLocallyConstant.hasIdentityPrinciple
+ IsLocallyConstant.isWeaklyLocallyConstant
+ IsLocallyInjective.isStalkInj
+ IsSeparated
+ IsStalkInj
+ IsStalkInj'
+ IsStalkInj.isStalkInj'
+ IsStalkInj.sheafify
+ IsStalkSurj
+ IsStalkSurj.sheafify
+ IsWeaklyLocallyConstant
+ IsWeaklyLocallyConstant.isSeparated
+ IsWeaklyLocallyConstant.isStalkSurj
+ LocalPredicate.pullback
+ LocallyEqSection
+ OpenPartialHomeomorph.isLocalHomeomorphOn
+ PrelocalPredicate.isStalkInj_iff
+ PrelocalPredicate.pullback
+ PrelocalPredicate.sheafifyOf
+ Pullback
+ Sheafify
+ TrivializationOn
+ adjunction
+ adjunctionPrelocalPredicate
+ arrowSigma
+ continuous_cod
+ continuous_cod_iff
+ continuous_cod_iff_of_opens
+ continuous_dom_iff
+ continuous_section
+ continuous_section_iff
+ continuous_sheafify_section
+ equiv
+ exists_eq_mk_of_comp_eq_id
+ exists_eq_mk_of_comp_eq_val
+ exists_section
+ homeomorph
+ homeomorphRangeSection
+ injOn_range_subtype_section
+ instance : TopologicalSpace (EtaleSpace P)
+ isConstantOn_iff
+ isContinuousSection
+ isCoveringMapOn
+ isCoveringMapOn_of_isLocallyConstant
+ isCoveringMap_of_isLocallyConstant
+ isEvenlyCovered
+ isLocalHomeomorphOn_proj
+ isLocalHomeomorph_iff_isLocallyInjective_continuous_isOpenMap
+ isLocalHomeomorph_proj
+ isLocal_sheafify
+ isOpenEmbedding_restrict
+ isOpenEmbedding_restrict_proj
+ isOpen_iff
+ isOpen_injOn_iff_exists_continuous_section
+ isOpen_injOn_tfae
+ isOpen_preimage_inter_range_section
+ isOpen_range_section
+ isOpen_range_section_opens_iff
+ isSeparatedMap_proj
+ isStalkInj_isGerm
+ isStalkSurj_isGerm
+ isTopologicalBasis
+ le_sheafify
+ mk
+ mk_piEquivSubtypeSigma_symm
+ mk_piSubtypeEquivSubtypeSigma
+ monodromy
+ piSubtypeEquivSubtypeSigma
+ pred_sec
+ preimage_snd_comp_equiv
+ proj
+ sec
+ sec_apply
+ sec_eq_of_pred
+ section_locallyEqSection_iff
+ sheafify_eq_iff
+ sigmaSubtypeComm
+ subtype_section_ext
+ symm_apply_coe
+ trivializationOn
++ isOpenEmbedding_section
++ isOpen_range_section_iff
- sheafifyOf
-++- stalkToFiber
-+-+ stalkToFiber_injective
-+-+ stalkToFiber_surjective

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).