From decf3af1d71ebb6c937acf47a651e002d6ddda08 Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Fri, 3 Apr 2026 14:24:34 +0200
Subject: [PATCH 1/7] small ind

---
 Mathlib/Topology/SmallInductiveDimension.lean | 65 +++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 Mathlib/Topology/SmallInductiveDimension.lean

diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean
new file mode 100644
index 00000000000000..4593f940eebdb7
--- /dev/null
+++ b/Mathlib/Topology/SmallInductiveDimension.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Fernando Chu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fernando Chu, Andrew Yang
+-/
+module
+
+public import Mathlib
+
+/-!
+# Small inductive dimension
+
+The small inductive dimension of a space is inductively defined as follows. Empty spaces have
+small inductive dimension less than 0, and a topological space has dimension less than `n + 1` if
+it has a topological basis whose elements have frontiers of dimension strictly less `n`.
+
+In this file we formalize this notion, and characterize the cases `n = 0` and `n = 1`.
+
+## Main definitions
+
+* `HasSmallInductiveDimensionLT X n` : Provides a class stating that `X` has small inductive
+  dimension less than `n`.
+* `HasSmallInductiveDimensionLE X n` : Provides an abbrev for
+  `HasSmallInductiveDimensionLT X (n + 1)`.
+
+## References
+
+* https://en.wikipedia.org/wiki/Inductive_dimension
+-/
+
+@[expose] public section
+
+open Set TopologicalSpace
+
+/- The small inductive dimension of a space is inductively defined as follows. Empty spaces have
+small inductive dimension less than 0, and a topological space has dimension less than `n + 1` if
+it has a topological basis whose elements have frontiers of dimension strictly less `n`. -/
+class inductive HasSmallInductiveDimensionLT.{u} :
+  ∀ (X : Type u) [TopologicalSpace X], ℕ → Prop where
+  | zero {X : Type u} [TopologicalSpace X] [IsEmpty X] : HasSmallInductiveDimensionLT X 0
+  | succ {X : Type u} [TopologicalSpace X] (n : ℕ) (s : Set (Set X)) (hs : IsTopologicalBasis s)
+      (h : ∀ U ∈ s, HasSmallInductiveDimensionLT ↑(frontier U) n) :
+      HasSmallInductiveDimensionLT X (n + 1)
+
+variable (X : Type) [TopologicalSpace X]
+
+/-- A topological space has dimension `≤ n` if it has dimension `< n + 1`. -/
+abbrev HasSmallInductiveDimensionLE (n : ℕ) :=
+  HasSmallInductiveDimensionLT X (n + 1)
+
+lemma HasSmallInductiveDimensionLT_zero_iff :
+    HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X :=
+  ⟨fun h ↦ by cases h; assumption, fun _ ↦ .zero⟩
+
+lemma HasSmallInductiveDimensionLT_one_iff :
+    HasSmallInductiveDimensionLT X 1 ↔ IsTopologicalBasis { s : Set X | IsClopen s } := by
+  constructor
+  · intro (.succ _ s hs h)
+    refine hs.of_isOpen_of_subset (fun _ hU ↦ hU.isOpen) (fun U hU ↦ ⟨?_, hs.isOpen hU⟩)
+    rw [← closure_subset_iff_isClosed]
+    cases h U hU
+    rwa [isEmpty_coe_sort, (hs.isOpen hU).frontier_eq, diff_eq_empty] at ‹_›
+  · exact fun h ↦ .succ 0 _ h fun _ hU ↦ hU.frontier_eq ▸ .zero
+
+end

From cf7dff7d872e808fb5a6c590035e74e2945b3ff1 Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Sat, 4 Apr 2026 00:26:36 +0200
Subject: [PATCH 2/7] review

---
 Mathlib/Topology/SmallInductiveDimension.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean
index 4593f940eebdb7..28c267ea996602 100644
--- a/Mathlib/Topology/SmallInductiveDimension.lean
+++ b/Mathlib/Topology/SmallInductiveDimension.lean
@@ -22,6 +22,7 @@ In this file we formalize this notion, and characterize the cases `n = 0` and `n
   dimension less than `n`.
 * `HasSmallInductiveDimensionLE X n` : Provides an abbrev for
   `HasSmallInductiveDimensionLT X (n + 1)`.
+* `smallInductiveDimension X` : The small inductive dimension of `X`, with values in `WithBot ℕ∞`.
 
 ## References
 
@@ -48,6 +49,10 @@ variable (X : Type) [TopologicalSpace X]
 abbrev HasSmallInductiveDimensionLE (n : ℕ) :=
   HasSmallInductiveDimensionLT X (n + 1)
 
+/-- The small inductive dimension of a topological space. -/
+noncomputable def smallInductiveDimension : WithBot ℕ∞ :=
+  sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < i → HasSmallInductiveDimensionLT X i}
+
 lemma HasSmallInductiveDimensionLT_zero_iff :
     HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X :=
   ⟨fun h ↦ by cases h; assumption, fun _ ↦ .zero⟩

From fd97d3f7c5f04b9916063021805b81091c517fe5 Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Sat, 4 Apr 2026 00:29:14 +0200
Subject: [PATCH 3/7] imports

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 8a1d84f580cf02..c4a052b6863768 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7801,6 +7801,7 @@ public import Mathlib.Topology.Sheaves.Sheafify
 public import Mathlib.Topology.Sheaves.Skyscraper
 public import Mathlib.Topology.Sheaves.Stalks
 public import Mathlib.Topology.ShrinkingLemma
+public import Mathlib.Topology.SmallInductiveDimension
 public import Mathlib.Topology.Sober
 public import Mathlib.Topology.Specialization
 public import Mathlib.Topology.Spectral.Basic

From 68e2daf45064f1b21a03ad22ee61aa3ee409797b Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Sat, 4 Apr 2026 06:26:00 +0200
Subject: [PATCH 4/7] imports

---
 Mathlib/Topology/SmallInductiveDimension.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean
index 28c267ea996602..ebaa275495c2b5 100644
--- a/Mathlib/Topology/SmallInductiveDimension.lean
+++ b/Mathlib/Topology/SmallInductiveDimension.lean
@@ -5,7 +5,9 @@ Authors: Fernando Chu, Andrew Yang
 -/
 module
 
-public import Mathlib
+public import Mathlib.Data.ENat.Lattice
+public import Mathlib.Topology.Bases
+public import Mathlib.Topology.Clopen
 
 /-!
 # Small inductive dimension

From aae4368865551e2e661e10056d2c041db247472d Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Sat, 4 Apr 2026 16:22:18 +0200
Subject: [PATCH 5/7] doc

---
 Mathlib/Topology/SmallInductiveDimension.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean
index ebaa275495c2b5..e143a40f127404 100644
--- a/Mathlib/Topology/SmallInductiveDimension.lean
+++ b/Mathlib/Topology/SmallInductiveDimension.lean
@@ -35,9 +35,9 @@ In this file we formalize this notion, and characterize the cases `n = 0` and `n
 
 open Set TopologicalSpace
 
-/- The small inductive dimension of a space is inductively defined as follows. Empty spaces have
+/-- The small inductive dimension of a space is inductively defined as follows. Empty spaces have
 small inductive dimension less than 0, and a topological space has dimension less than `n + 1` if
-it has a topological basis whose elements have frontiers of dimension strictly less `n`. -/
+it has a topological basis whose elements have frontiers of dimension strictly less `n`. --/
 class inductive HasSmallInductiveDimensionLT.{u} :
   ∀ (X : Type u) [TopologicalSpace X], ℕ → Prop where
   | zero {X : Type u} [TopologicalSpace X] [IsEmpty X] : HasSmallInductiveDimensionLT X 0

From 9ff09317a6f04fb61c695cfcd675ed75da362600 Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Sat, 4 Apr 2026 16:41:32 +0200
Subject: [PATCH 6/7] doc

---
 Mathlib/Topology/SmallInductiveDimension.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean
index e143a40f127404..24e8316ce0b3d5 100644
--- a/Mathlib/Topology/SmallInductiveDimension.lean
+++ b/Mathlib/Topology/SmallInductiveDimension.lean
@@ -35,9 +35,11 @@ In this file we formalize this notion, and characterize the cases `n = 0` and `n
 
 open Set TopologicalSpace
 
-/-- The small inductive dimension of a space is inductively defined as follows. Empty spaces have
+/--
+The small inductive dimension of a space is inductively defined as follows. Empty spaces have
 small inductive dimension less than 0, and a topological space has dimension less than `n + 1` if
-it has a topological basis whose elements have frontiers of dimension strictly less `n`. --/
+it has a topological basis whose elements have frontiers of dimension strictly less `n`.
+-/
 class inductive HasSmallInductiveDimensionLT.{u} :
   ∀ (X : Type u) [TopologicalSpace X], ℕ → Prop where
   | zero {X : Type u} [TopologicalSpace X] [IsEmpty X] : HasSmallInductiveDimensionLT X 0

From 49d923412b4085a07aa4fcbff9775e7d963a25e7 Mon Sep 17 00:00:00 2001
From: FernandoChu <17756312+FernandoChu@users.noreply.github.com>
Date: Sat, 4 Apr 2026 16:59:32 +0200
Subject: [PATCH 7/7] doc

---
 Mathlib/Topology/SmallInductiveDimension.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/SmallInductiveDimension.lean b/Mathlib/Topology/SmallInductiveDimension.lean
index 24e8316ce0b3d5..c4dc258d790162 100644
--- a/Mathlib/Topology/SmallInductiveDimension.lean
+++ b/Mathlib/Topology/SmallInductiveDimension.lean
@@ -36,9 +36,10 @@ In this file we formalize this notion, and characterize the cases `n = 0` and `n
 open Set TopologicalSpace
 
 /--
-The small inductive dimension of a space is inductively defined as follows. Empty spaces have
-small inductive dimension less than 0, and a topological space has dimension less than `n + 1` if
-it has a topological basis whose elements have frontiers of dimension strictly less `n`.
+For a topological space, the property of having small inductive dimension less than `n : ℕ`  is
+inductively defined as follows. Empty spaces have small inductive dimension less than 0, and a
+topological space has dimension less than `n + 1` if it has a topological basis whose elements have
+frontiers of dimension strictly less `n`.
 -/
 class inductive HasSmallInductiveDimensionLT.{u} :
   ∀ (X : Type u) [TopologicalSpace X], ℕ → Prop where