Theorem Topology.IsInducing.hasSmallInductiveDimensionLE

Modification history

2026-10-08 09:22
Mathlib/Topology/InductiveDimension/Functions.lean
chore: split `Topology.SmallInductiveDimension` (#44617) …
Modified Topology.IsInducing.hasSmallInductiveDimensionLEView on Github →
2026-08-25 15:52
Mathlib/Topology/SmallInductiveDimension.lean
feat(Topology): small inductive dimension does not increase under inducing maps (#42167) …
Added Topology.IsInducing.hasSmallInductiveDimensionLEView on Github →