feat: HasSmallInductiveDimensionLT is monotonic (leanprover-community#40897)

We prove that `HasSmallInductiveDimensionLT m` implies `HasSmallInductiveDimensionLT n` whenever `m ≤ n`.

Author: vihdzp

Mathlib/Topology/SmallInductiveDimension.lean

@@ -79,4 +79,25 @@ lemma hasSmallInductiveDimensionLT_one_iff :
 @[deprecated (since := "2026-06-21")]
 alias HasSmallInductiveDimensionLT_one_iff := hasSmallInductiveDimensionLT_one_iff
 
-end
+theorem HasSmallInductiveDimensionLT.mono {m n : ℕ} (hmn : m ≤ n)
+    (H : HasSmallInductiveDimensionLT X m) : HasSmallInductiveDimensionLT X n := by
+  induction n generalizing m X with
+  | zero => simp_all
+  | succ m IH =>
+    cases H with
+    | zero => exact .succ _ ∅ (by simpa) (by simp)
+    | succ n s hs h =>
+      refine .succ _ s hs fun U hU ↦ IH ?_ (h U hU)
+      rwa [add_le_add_iff_right] at hmn
+
+theorem HasSmallInductiveDimensionLE.mono {m n : ℕ} (hmn : m ≤ n)
+    (H : HasSmallInductiveDimensionLE X m) : HasSmallInductiveDimensionLE X n := by
+  apply HasSmallInductiveDimensionLT.mono _ H
+  rwa [add_le_add_iff_right]
+
+theorem HasSmallInductiveDimensionLT.hasSmallInductiveDimensionLE {n : ℕ}
+    (H : HasSmallInductiveDimensionLT X n) : HasSmallInductiveDimensionLE X n :=
+  HasSmallInductiveDimensionLT.mono n.le_succ H
+
+instance (n : ℕ) [IsEmpty X] : HasSmallInductiveDimensionLT X n :=
+  .mono zero_le <| hasSmallInductiveDimensionLT_zero_iff.2 ‹_›