Theorems · Definition · category theory

Profinite.NobelingProof.spanCone

{I : Type u} →
  {C : Set (I → Bool)} →
    [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] →
      (hC : IsCompact C) → CategoryTheory.Limits.Cone (Profinite.NobelingProof.spanFunctor hC)

The limit cone on spanFunctor with point C.

Defined in: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Decidable

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement and proof · cited by 13,712
Oppositestatement and proof · cited by 8,081
Set.Elemproof · cited by 7,166
TopCat.carrierstatement · cited by 3,184
Opposite.unopproof · cited by 2,231
TopCatstatement · cited by 1,889
IsCompactstatement and proof · cited by 1,282
CategoryTheory.Limits.Conestatement · cited by 710
TotallyDisconnectedSpacestatement · cited by 295
Profinitestatement · cited by 75
CategoryTheory.ConcreteCategory.ofHomproof · cited by 18

Cited by2

Results whose statement or proof uses this declaration.

Profinite.NobelingProof.spanCone_isLimitstatement and proof · cited by 1
Profinite.NobelingProof.fin_comap_jointlySurjectiveproof · cited by 1