Theorems · Definition · general topology

HasSmallInductiveDimensionLT.recOn

∀ {motive : (X : Type u) → [inst : TopologicalSpace X] → (a : ℕ) → HasSmallInductiveDimensionLT X a → Prop} {X : Type u}
  [inst : TopologicalSpace X] {a : ℕ} (t : HasSmallInductiveDimensionLT X a),
  (∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : IsEmpty X], motive X 0 ⋯) →
    (∀ {X : Type u} [inst : TopologicalSpace X] (n : ℕ) (s : Set (Set X)) (hs : TopologicalSpace.IsTopologicalBasis s)
        (h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) n),
        (∀ (U : Set X) (a : U ∈ s), motive (↑(frontier U)) n ⋯) → motive X (n + 1) ⋯) →
      motive X a t

Defined in

Mathlib.Topology.SmallInductiveDimension

Cited by

0 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace