feat(topology): Small inductive dimension

[FernandoChu]

Adds a type class for small inductive dimension. See also #37444.

Co-authored-by: Andrew Yang the.erd.one@gmail.com

AI disclosure: Claude code assisted in preparing this PR.

---

[github-actions]

PR summary 205a0ba54c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.SmallInductiveDimension (new file)	733

---

Declarations diff

+ HasSmallInductiveDimensionLE
+ HasSmallInductiveDimensionLT_one_iff
+ HasSmallInductiveDimensionLT_zero_iff
+ inductive
+ smallInductiveDimension

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[vihdzp]

It seems a bit weird to me to have a typeclass for "small inductive dimension less than", but not an actual definition for the small inductive dimension.

[FernandoChu]

I was following the sSet case, but this seems to be the exception, not the norm. I've added a def, thanks!