Theorems · Definition · category theory

Profinite.indexCone_isLimit

{ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [inst_1 : ∀ (i : ι), T2Space (X i)] →
          [inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)] →
            (hC : IsCompact C) → CategoryTheory.Limits.IsLimit (Profinite.indexCone hC)

indexCone is a limit cone.

Defined in

Mathlib.Topology.Category.Profinite.Product

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceTotallyDisconnectedSpace