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).
• smallInductiveDimension X : The small inductive dimension of X, with values in WithBot ℕ∞.

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) [TopologicalSpace X] (n : ℕ) : Prop

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

Equations

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

noncomputable def smallInductiveDimension (X : Type) [TopologicalSpace X] : WithBot ℕ∞

The small inductive dimension of a topological space.

Equations

• smallInductiveDimension X = sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i}

theorem HasSmallInductiveDimensionLT_zero_iff (X : Type) [TopologicalSpace X] : HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X

theorem HasSmallInductiveDimensionLT_one_iff (X : Type) [TopologicalSpace X] : HasSmallInductiveDimensionLT X 1 ↔ TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}