Theorem smallInductiveDimension_of_isEmpty

Modification history

2026-10-08 09:22
Mathlib/Topology/InductiveDimension/Functions.lean
chore: split `Topology.SmallInductiveDimension` (#44617) …
Modified smallInductiveDimension_of_isEmptyView on Github →
2026-07-29 08:56
Mathlib/Topology/SmallInductiveDimension.lean
feat: lemmas about the `smallInductiveDimension` (#40879) …
Added smallInductiveDimension_of_isEmptyView on Github →