Theorem smallInductiveDimension_subtype_le

Modification history

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