@[reducible, inline]

noncomputable abbrev dimension (X : Type u_1) [TopologicalSpace X] : WithBot ℕ∞

The dimension of a topological space X (Definition 11): the length of the longest chain of irreducible closed subsets, modeled here via the topological Krull dimension.

theorem dimension_eq_krullDim_irreducibleCloseds (X : Type u_1) [TopologicalSpace X] : dimension X = Order.krullDim (TopologicalSpace.IrreducibleCloseds X)

The dimension of X equals the Krull dimension of its poset of irreducible closed subsets, by definition.

theorem dimension_le_of_isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsInducing f) : dimension Y ≤ dimension X

Dimension is monotone under topological inducing maps.

theorem dimension_subspace_le (X : Type u_1) [TopologicalSpace X] (Y : Set X) : dimension ↑Y ≤ dimension X

A subspace has dimension at most that of the ambient space.

theorem dimension_le_zero_of_discreteTopology (X : Type u_1) [TopologicalSpace X] [DiscreteTopology X] : dimension X ≤ 0

A discrete topological space has dimension at most zero.