Theorem smallInductiveDimension_eq

Modification history

2026-10-08 09:22

Mathlib/Topology/InductiveDimension/Functions.lean

chore: split `Topology.SmallInductiveDimension` (#44617) …

Modified smallInductiveDimension_eq View on Github →

2026-07-29 08:56

Mathlib/Topology/SmallInductiveDimension.lean

feat: lemmas about the `smallInductiveDimension` (#40879) …

Added smallInductiveDimension_eq View on Github →