Compact

📁 Source: Mathlib/Topology/Algebra/Group/Compact.lean

Statistics

Metric	Count
Definitions	0
Theorems locallyCompactSpace_of_addGroup, locallyCompactSpace_of_group	2
Total	2

TopologicalSpace.PositiveCompacts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace_of_addGroup 📖	mathematical	—	LocallyCompactSpace	—	interior_nonempty IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup isCompact mem_interior_iff_mem_nhds
locallyCompactSpace_of_group 📖	mathematical	—	LocallyCompactSpace	—	interior_nonempty IsCompact.locallyCompactSpace_of_mem_nhds_of_group isCompact mem_interior_iff_mem_nhds

---

← Back to Index