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.

See the Topology.InductiveDimension.Functions file for the WithBot ℕ∞-valued smallInductiveDimension function.

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).

TODO

Formalize the large inductive dimension as well.

References

• https://en.wikipedia.org/wiki/Inductive_dimension

class inductive HasSmallInductiveDimensionLT (X : Type u) [TopologicalSpace X] : ℕ → Prop

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.

• zero {X : Type u} [TopologicalSpace X] [IsEmpty X] : HasSmallInductiveDimensionLT X 0
• succ {X : Type u} [TopologicalSpace X] (n : ℕ) (s : Set (Set X)) (hs : TopologicalSpace.IsTopologicalBasis s) (h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) n) : HasSmallInductiveDimensionLT X (n + 1)

@[reducible, inline]

abbrev HasSmallInductiveDimensionLE (X : Type u_1) [TopologicalSpace X] (n : ℕ) : Prop

A topological space has dimension ≤ n if it has dimension < n + 1.

Equations

• HasSmallInductiveDimensionLE X n = HasSmallInductiveDimensionLT X (n + 1)

@[simp]

theorem hasSmallInductiveDimensionLT_zero_iff {X : Type u_1} [TopologicalSpace X] : HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X

@[deprecated hasSmallInductiveDimensionLT_zero_iff (since := "2026-06-21")]

theorem HasSmallInductiveDimensionLT_zero_iff {X : Type u_1} [TopologicalSpace X] : HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X

Alias of hasSmallInductiveDimensionLT_zero_iff.

theorem HasSmallInductiveDimensionLT.mono {X : Type u_1} [TopologicalSpace X] {m n : ℕ} (hmn : m ≤ n) (H : HasSmallInductiveDimensionLT X m) : HasSmallInductiveDimensionLT X n

theorem HasSmallInductiveDimensionLE.mono {X : Type u_1} [TopologicalSpace X] {m n : ℕ} (hmn : m ≤ n) (H : HasSmallInductiveDimensionLE X m) : HasSmallInductiveDimensionLE X n

theorem HasSmallInductiveDimensionLT.hasSmallInductiveDimensionLE {X : Type u_1} [TopologicalSpace X] {n : ℕ} (H : HasSmallInductiveDimensionLT X n) : HasSmallInductiveDimensionLE X n

instance instHasSmallInductiveDimensionLTOfIsEmpty {X : Type u_1} [TopologicalSpace X] (n : ℕ) [IsEmpty X] : HasSmallInductiveDimensionLT X n

Zero-dimensional spaces

@[reducible, inline]

abbrev ZeroDimensionalSpace (X : Type u_1) [TopologicalSpace X] : Prop

A zero-dimensional topological space is defined as one with small inductive dimension ≤ 0. In particular, our definition of ZeroDimensionalSpace allows the empty space even though, strictly speaking, it is (-1)-dimensional.

An equivalent characterization is that a zero-dimensional space is one with a basis of clopen sets.

Equations

• ZeroDimensionalSpace X = HasSmallInductiveDimensionLT X 1

theorem zeroDimensionalSpace_def {X : Type u_1} [TopologicalSpace X] : ZeroDimensionalSpace X ↔ HasSmallInductiveDimensionLT X 1

theorem zeroDimensionalSpace_def' {X : Type u_1} [TopologicalSpace X] : ZeroDimensionalSpace X ↔ HasSmallInductiveDimensionLE X 0

theorem zeroDimensionalSpace_iff_isTopologicalBasis_isClopen {X : Type u_1} [TopologicalSpace X] : ZeroDimensionalSpace X ↔ TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

@[deprecated zeroDimensionalSpace_iff_isTopologicalBasis_isClopen (since := "2026-10-08")]

theorem hasSmallInductiveDimensionLT_one_iff {X : Type u_1} [TopologicalSpace X] : ZeroDimensionalSpace X ↔ TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

Alias of zeroDimensionalSpace_iff_isTopologicalBasis_isClopen.

@[deprecated zeroDimensionalSpace_iff_isTopologicalBasis_isClopen (since := "2026-06-21")]

theorem HasSmallInductiveDimensionLT_one_iff {X : Type u_1} [TopologicalSpace X] : ZeroDimensionalSpace X ↔ TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

Alias of zeroDimensionalSpace_iff_isTopologicalBasis_isClopen.

theorem isTopologicalBasis_isClopen {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

theorem ZeroDimensionalSpace.of_isTopologicalBasis {X : Type u_1} [TopologicalSpace X] {u : Set (Set X)} (hs : ∀ s ∈ u, IsClopen s) (hu : TopologicalSpace.IsTopologicalBasis u) : ZeroDimensionalSpace X

theorem zeroDimensionalSpace_iff_nhds_hasBasis_isClopen {X : Type u_1} [TopologicalSpace X] : ZeroDimensionalSpace X ↔ ∀ (x : X), (nhds x).HasBasis (fun (s : Set X) => IsClopen s ∧ x ∈ s) id

theorem nhds_basis_isClopen {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => IsClopen s ∧ x ∈ s) id

@[deprecated nhds_basis_isClopen (since := "2026-10-08")]

theorem nhds_basis_clopen {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsClopen s) id

theorem exists_isClopen_mem_of_isOpen {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) : ∃ (V : Set X), IsClopen V ∧ x ∈ V ∧ V ⊆ U

@[deprecated exists_isClopen_mem_of_isOpen (since := "2026-10-08")]

theorem compact_exists_isClopen_in_isOpen {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) : ∃ (V : Set X), IsClopen V ∧ x ∈ V ∧ V ⊆ U

Alias of exists_isClopen_mem_of_isOpen.

theorem ZeroDimensionalSpace.of_hasBasis {X : Type u_1} [TopologicalSpace X] (H : ∀ (x : X), ∃ (ι : Sort u_3) (p : ι → Prop) (s : ι → Set X), (∀ (i : ι), p i → IsClopen (s i)) ∧ (nhds x).HasBasis p s) : ZeroDimensionalSpace X

instance instZeroDimensionalSpaceOfDiscreteTopology {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : ZeroDimensionalSpace X

instance instZeroDimensionalSpaceOfIndiscreteTopology {X : Type u_1} [TopologicalSpace X] [IndiscreteTopology X] : ZeroDimensionalSpace X

theorem exists_clopen_of_closed_subset_open {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] [CompactSpace X] {Z U : Set X} (hZ : IsClosed Z) (hU : IsOpen U) (hZU : Z ⊆ U) : ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U

In a zero-dimensional compact space X, if Z ⊆ U are subsets with Z closed and U open, there exists a clopen C with Z ⊆ C ⊆ U.

theorem exists_clopen_partition_of_clopen_cover {X : Type u_1} [TopologicalSpace X] [ZeroDimensionalSpace X] [CompactSpace X] {I : Type u_3} [Finite I] {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i)) (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : Set.univ.PairwiseDisjoint Z) : ∃ (C : I → Set X), (∀ (i : I), IsClopen (C i)) ∧ (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ (i : I), D i ⊆ ⋃ (i : I), C i ∧ Set.univ.PairwiseDisjoint C

Let X be a zero-dimensional compact Hausdorff space, D i ⊆ X a finite family of clopens, and Z i ⊆ D i closed. Assume that the Z i are pairwise disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i with the C i disjoint, and such that ∪ D i ⊆ ∪ C i.