feat(Topology/KrullDimension): add subspace dimension inequality

[ADA-Projects]

This PR extends topological Krull dimension theory with basic results about subspaces.

• Add mapIrreducibleClosed function for canonical maps between irreducible closed sets
• Prove injectivity and strict monotonicity of these maps
• Establish partial order structure on IrreducibleCloseds
• Prove topKrullDim_subspace_le theorem showing dim(Y) ≤ dim(X) for subspaces

Update (per reviewer feedback):

Reorganized code structure as requested:

• Moved IrreducibleCloseds extensions from KrullDimension.lean to Sets/Closeds.lean
• This includes PartialOrder instance, map functions, and embedding lemmas
• Better modularity: other files can now use IrreducibleCloseds without importing Krull dimension theory

The main result topologicalKrullDim_subspace_le remains the same - any subspace Y has dim(Y) ≤ dim(X).

Some sections of this code (and documentation) were generated with the help of Gemini.

Update 2

Addressed reviewer feedback with the following improvements:

• Simplify IrreducibleCloseds.map to work with any continuous function
  (no longer requires closed maps)
• Add coe_map lemma
• Rename lemmas from mapOfEmbedding_* to map_*_of_isEmbedding for
  consistency with Mathlib naming conventions
• Use inferInstance for PartialOrder instance on IrreducibleCloseds
• Merge variable declarations in Sets/Closeds.lean
• Add necessary imports (Topology.Defs.Induced)
• Open Topology namespace for cleaner code
• Remove unnecessary wrappers in 'Sets/Closeds.lean'

Update 3

Addressed and integrated reviewer feedback:

• Use IsInducing instead of IsEmbedding in dimension theorems
• Rename map_of_isEmbedding to map_of_isInducing
• Simplify map_injective_of_isInducing proof using SetLike.coe_injective
• Simplify map_strictMono_of_isInducing using Monotone.strictMono_of_injective
• Add deprecation alias for IsClosedEmbedding.topologicalKrullDim_le
• Remove redundant PartialOrder instance (already inferred)

The main theorem topologicalKrullDim_subspace_le remains unchanged.

---

[github-actions]

PR summary 1838dfbf5d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsInducing.topologicalKrullDim_le
+ coe_map
+ map
+ map_injective_of_isInducing
+ map_mono
+ map_strictMono_of_isInducing
+ topologicalKrullDim_subspace_le
- IrreducibleCloseds.map
- IrreducibleCloseds.map_strictMono

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

[fpvandoorn]

If you think you have addressed all the review comments, please remove the label awaiting-author by writing a comment with the text -awaiting-author.

[ADA-Projects]

-awaiting-author

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[ADA-Projects]

-awaiting-author

[erdOne]

I think you have messed up something. Can you try merging master again?

[erdOne]

Thanks for the great PR and for the patience!
maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[ADA-Projects]

I've done 'lake build Mathlib' and everything works fine in my fork. Why did the CI test fail? it seems the cache of the files I've modified is missing.

[erdOne]

Can you try merging master? It might be an issue about a change in CI.