Commit 2026-07-29 08:56 e91869b3

View on Github →

feat: lemmas about the smallInductiveDimension (#40879) We prove various lemmas about the smallInductiveDimension of a topological space, as well as interactions with the HasSmallInductiveDimensionLT and HasSmallInductiveDimensionLE typeclasses.

Estimated changes

Modified Mathlib/Topology/SmallInductiveDimension.lean

modified theorem hasSmallInductiveDimensionLT_zero_iff

added theorem smallInductiveDimension_eq

added theorem smallInductiveDimension_eq_bot

added theorem smallInductiveDimension_le

added theorem smallInductiveDimension_le_iff

added theorem smallInductiveDimension_lt

added theorem smallInductiveDimension_lt_iff

added theorem smallInductiveDimension_of_isEmpty