Commit 2026-07-17 19:29 ce279564

View on Github →

feat: HasSmallInductiveDimensionLT is monotonic (#40897) We prove that HasSmallInductiveDimensionLT m implies HasSmallInductiveDimensionLT n whenever m ≤ n.

Estimated changes

Modified Mathlib/Topology/SmallInductiveDimension.lean

added theorem HasSmallInductiveDimensionLE.mono

added theorem HasSmallInductiveDimensionLT.hasSmallInductiveDimensionLE

added theorem HasSmallInductiveDimensionLT.mono