Commit 2026-10-08 09:22 4a3cff2c

chore: split Topology.SmallInductiveDimension (#44617) The imports relating to ℕ∞ have turned out to be too heavy for topology. So we split the parts of the file that depend on this and the parts that don't. We've named the folder InductiveDimension and not SmallInductiveDimension, in anticipation that we'll at some point formalize the large inductive dimension as well.