Small inductive dimension

This file defines a WithBot ℕ∞-valued function which measures the small inductive dimension of a topological space, and connects it to the HasSmallInductiveDimensionLT and HasSmallInductiveDimensionLE typeclasses defined in Topology.InductiveDimension.Classes.

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

The small inductive dimension of a topological space.

Equations

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

theorem smallInductiveDimension_le_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} : smallInductiveDimension X ≤ ↑n ↔ HasSmallInductiveDimensionLE X n

theorem smallInductiveDimension_lt_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} : smallInductiveDimension X < ↑n ↔ HasSmallInductiveDimensionLT X n

theorem smallInductiveDimension_le (X : Type u_1) [TopologicalSpace X] (n : ℕ) [H : HasSmallInductiveDimensionLE X n] : smallInductiveDimension X ≤ ↑n

theorem smallInductiveDimension_lt (X : Type u_1) [TopologicalSpace X] (n : ℕ) [H : HasSmallInductiveDimensionLT X n] : smallInductiveDimension X < ↑n

theorem smallInductiveDimension_eq {X : Type u_1} [TopologicalSpace X] (n : ℕ) (hle : HasSmallInductiveDimensionLE X n) (hlt : ¬HasSmallInductiveDimensionLT X n) : smallInductiveDimension X = ↑n

@[simp]

theorem smallInductiveDimension_eq_bot {X : Type u_1} [TopologicalSpace X] : smallInductiveDimension X = ⊥ ↔ IsEmpty X

@[simp]

theorem smallInductiveDimension_of_isEmpty (X : Type u_1) [TopologicalSpace X] [IsEmpty X] : smallInductiveDimension X = ⊥

theorem Topology.IsInducing.hasSmallInductiveDimensionLT {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) {n : ℕ} (h : HasSmallInductiveDimensionLT Y n) : HasSmallInductiveDimensionLT X n

theorem Topology.IsInducing.hasSmallInductiveDimensionLE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) {n : ℕ} (h : HasSmallInductiveDimensionLE Y n) : HasSmallInductiveDimensionLE X n

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

The small inductive dimension does not increase under inducing maps.

theorem smallInductiveDimension_subtype_le {X : Type u_1} [TopologicalSpace X] {p : X → Prop} : smallInductiveDimension { x : X // p x } ≤ smallInductiveDimension X

The small inductive dimension of a subspace is at most that of the ambient space.

theorem Homeomorph.hasSmallInductiveDimensionLT {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (n : ℕ) : HasSmallInductiveDimensionLT X n ↔ HasSmallInductiveDimensionLT Y n

theorem Homeomorph.hasSmallInductiveDimensionLE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (n : ℕ) : HasSmallInductiveDimensionLE X n ↔ HasSmallInductiveDimensionLE Y n

instance instHasSmallInductiveDimensionLTSubtype {X : Type u_1} [TopologicalSpace X] {p : X → Prop} (n : ℕ) [h : HasSmallInductiveDimensionLT X n] : HasSmallInductiveDimensionLT (Subtype p) n

theorem Homeomorph.smallInductiveDimension_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) : smallInductiveDimension X = smallInductiveDimension Y

The small inductive dimension is preserved by homeomorphisms.