Konig

📁 Source: Mathlib/Topology/Category/TopCat/Limits/Konig.lean

Statistics

Metric	Count
Definitions partialSections	1
Theorems nonempty_limitCone_of_compact_t2_cofiltered_system, closed, directed, nonempty	4
Total	5

TopCat

Definitions

Name	Category	Theorems
partialSections 📖	CompOp	3 math math: partialSections.closed, partialSections.directed, partialSections.nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_limitCone_of_compact_t2_cofiltered_system 📖	mathematical	carrier CategoryTheory.Functor.obj TopCat instCategory CompactSpace str T2Space	CategoryTheory.Limits.Cone.pt limitCone	—	IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed partialSections.directed partialSections.nonempty IsClosed.isCompact Pi.compactSpace partialSections.closed Finset.mem_singleton_self

TopCat.partialSections

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closed 📖	mathematical	T2Space TopCat.carrier CategoryTheory.Functor.obj TopCat TopCat.instCategory TopCat.str	IsClosed Pi.topologicalSpace TopCat.partialSections	—	Set.ext Set.iInter_congr_Prop isClosed_biInter isClosed_eq Continuous.comp' ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass continuous_apply
directed 📖	mathematical	—	Directed Set Set.instHasSubset TopCat.partialSections Finset	—	Finset.mem_union_left Finset.mem_union_right Finset.mem_image
nonempty 📖	mathematical	TopCat.carrier CategoryTheory.Functor.obj TopCat TopCat.instCategory	Set.Nonempty TopCat.partialSections	—	isEmpty_or_nonempty TopCat.comp_app CategoryTheory.Functor.map_comp CategoryTheory.IsCofiltered.infTo_commutes

---

← Back to Index