LocallyFinite

📁 Source: Mathlib/Topology/Compactness/LocallyFinite.lean

Statistics

Metric	Count
Definitions fintypeOfCompact	1
Theorems finite_nonempty_inter_compact, finite_nonempty_of_compact, finite_of_compact	3
Total	4

LocallyFinite

Definitions

Name	Category	Theorems
fintypeOfCompact 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_nonempty_inter_compact 📖	mathematical	LocallyFinite IsCompact	Set.Finite setOf Set.Nonempty Set Set.instInter	—	IsCompact.elim_nhds_subcover Set.Finite.subset Set.Finite.biUnion Finset.finite_toSet Set.mem_iUnion₂ Set.mem_biUnion
finite_nonempty_of_compact 📖	mathematical	LocallyFinite	Set.Finite setOf Set.Nonempty	—	Set.inter_univ finite_nonempty_inter_compact isCompact_univ
finite_of_compact 📖	mathematical	LocallyFinite Set.Nonempty	Set.Finite Set.univ	—	finite_nonempty_of_compact

---

← Back to Index