Mathlib Map

Theorems · Definition · category theory

Profinite.NobelingProof.spanCone_isLimit

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

spanCone is a limit cone.

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

Around this declaration

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

Profinite.NobelingProof.fin_comap_jointlySurjective · cited by 1NobelingProof.fin_comap_j…DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetFinset · cited by 13712FinsetOpposite · cited by 8081OppositeTopCat.carrier · cited by 3184TopCat.carrierTopCat · cited by 1889TopCatCategoryTheory.Limits.Cone.pt · cited by 1298Cone.ptIsCompact · cited by 1282IsCompactCategoryTheory.Iso.refl · cited by 727Iso.reflCategoryTheory.Limits.IsLimit · cited by 664Limits.IsLimitTotallyDisconnectedSpace · cited by 295TotallyDisconnectedSpaceProfinite · cited by 75ProfiniteCategoryTheory.Limits.IsLimit.ofIsoLimit · cited by 39IsLimit.ofIsoLimitCategoryTheory.Limits.Cone.ext · cited by 34Cone.extCategoryTheory.Limits.IsLimit.postcomposeHomEquiv · cited by 14IsLimit.postcomposeHomEqu…NobelingProof.spanCone_isLimitCITED BYCITES

Cites20

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

Cited by1

Results whose statement or proof uses this declaration.