Hausdorff codimension

DefinitionLower bound on Hausdorff codimension#✓fully proved

Let \(S\) be a subset of an extended metric space and let \(n, c\) be natural numbers. The set \(S\) has Hausdorff codimension at least \(c\) in dimension \(n\) if \(S\) is empty or its Hausdorff dimension satisfies \(\dim_H S + c \le n\), the inequality being taken in \([0, \infty]\).

The empty-set case plays the role of the convention \(\dim_H \emptyset = -\infty\).

def HasHausdorffCodimAtLeast (S : Set X) (n c : ℕ) : Prop :=
  S = ∅ ∨ dimH S + (c : ℝ≥0∞) ≤ (n : ℝ≥0∞)

Used by 5

Used bySets of codimension larger than the dimension are empty · The empty set has every codimension · Characterization of Hausdorff codimension · A dimension bound gives a codimension bound · Subsets inherit a codimension bound

TheoremThe empty set has every codimension#✓fully proved

In an extended metric space, the empty set has Hausdorff codimension at least \(c\) in dimension \(n\) for all natural numbers \(n\) and \(c\).

theorem hasHausdorffCodimAtLeast_empty (n c : ℕ) :
    (∅ : Set X).HasHausdorffCodimAtLeast n c

Uses 1

Statement usesLower bound on Hausdorff codimension

TheoremSubsets inherit a codimension bound#✓fully proved

Let \(T \subseteq S\) be subsets of an extended metric space and let \(n, c\) be natural numbers. If \(S\) has Hausdorff codimension at least \(c\) in dimension \(n\), then so does \(T\).

theorem HasHausdorffCodimAtLeast.mono {S T : Set X} {n c : ℕ}
    (hS : S.HasHausdorffCodimAtLeast n c) (hTS : T ⊆ S) :
    T.HasHausdorffCodimAtLeast n c

Uses 1

Statement usesLower bound on Hausdorff codimension

TheoremSets of codimension larger than the dimension are empty#✓fully proved

Let \(S\) be a subset of an extended metric space and let \(n < c\) be natural numbers. If \(S\) has Hausdorff codimension at least \(c\) in dimension \(n\), then \(S\) is empty.

theorem HasHausdorffCodimAtLeast.eq_empty_of_lt {S : Set X} {n c : ℕ}
    (hS : S.HasHausdorffCodimAtLeast n c) (hlt : n < c) : S = ∅

Uses 1

Statement usesLower bound on Hausdorff codimension

TheoremA dimension bound gives a codimension bound#✓fully proved

Let \(S\) be a subset of an extended metric space and let \(c \le n\) be natural numbers. If the Hausdorff dimension of \(S\) satisfies \(\dim_H S \le n - c\), then \(S\) has Hausdorff codimension at least \(c\) in dimension \(n\).

theorem hasHausdorffCodimAtLeast_of_dimH_le {S : Set X} {n c : ℕ}
    (hcn : c ≤ n) (hdim : dimH S ≤ ((n - c : ℕ) : ℝ≥0∞)) :
    S.HasHausdorffCodimAtLeast n c

Uses 1 · Used by 1

Statement usesLower bound on Hausdorff codimension

Used byCharacterization of Hausdorff codimension

TheoremCharacterization of Hausdorff codimension#✓fully proved

Let \(S\) be a subset of an extended metric space and let \(n, c\) be natural numbers. Then \(S\) has Hausdorff codimension at least \(c\) in dimension \(n\) if and only if either \(S\) is empty, or both \(c \le n\) and the Hausdorff dimension of \(S\) satisfies \(\dim_H S \le n - c\).

theorem hasHausdorffCodimAtLeast_iff {S : Set X} {n c : ℕ} :
    S.HasHausdorffCodimAtLeast n c ↔
      S = ∅ ∨ (c ≤ n ∧ dimH S ≤ ((n - c : ℕ) : ℝ≥0∞))

Uses 2

Statement usesLower bound on Hausdorff codimension

Proof usesA dimension bound gives a codimension bound

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.