def HasLebesgueCoveringDimensionLE (X : Type u_1) [TopologicalSpace X] (n : ℕ) : Prop

A topological space X has Lebesgue covering dimension at most n if every finite open cover of X admits a finite open refinement in which no point of X is contained in more than n + 1 elements.

Equations

• One or more equations did not get rendered due to their size.

def HasLebesgueCoveringDimensionEq (X : Type u_1) [TopologicalSpace X] (n : ℕ) : Prop

A topological space X has Lebesgue covering dimension exactly n if it has covering dimension at most n but not at most n - 1.

Equations

• HasLebesgueCoveringDimensionEq X n = (HasLebesgueCoveringDimensionLE X n ∧ ∀ m < n, ¬HasLebesgueCoveringDimensionLE X m)