Compactness

📁 Source: Mathlib/Combinatorics/Compactness.lean

Statistics

Metric	Count
Definitions	0
Theorems rado_selection, rado_selection_subtype, rado_selection, rado_selection_subtype	4
Total	4

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rado_selection 📖	mathematical	Finite	Finset instHasSubset	—	discreteTopology_bot IsClosed.preimage continuous_restrict isClosed_discrete Pi.discreteTopology Finite.of_fintype Set.iInter_congr_Prop subset_biUnion_of_mem CompactSpace.iInter_nonempty Pi.compactSpace Finite.compactSpace
rado_selection_subtype 📖	mathematical	Finite	Finset instHasSubset SetLike.instMembership instSetLike Set.inclusion SetLike.coe	—	rado_selection

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rado_selection 📖	mathematical	Finite	Set Set.Finite Set.instHasSubset	—	Finset.finite_toSet Finset.rado_selection
rado_selection_subtype 📖	mathematical	Finite	Set Set.Finite Set.instHasSubset Set.instMembership Set.inclusion	—	Finset.finite_toSet Finset.rado_selection_subtype

---

← Back to Index