Theorems · Inductive type · general topology

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.

Defined in

Mathlib.Topology.SmallInductiveDimension

Cited by

9 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace