OAI/Topology/ArtinGroups/Realizations/FiniteWeightsCompact.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- instance
OAI.HarmonicArtin.finiteWeightsCompactline 14 - lemma
OAI.HarmonicArtin.weightFiniteInclusion_closedEmbeddingline 30 - lemma
OAI.HarmonicArtin.weightRestrict_continuous_finiteline 36 - theorem
OAI.HarmonicArtin.compact_map_finite_carrierline 43 - theorem
OAI.HarmonicArtin.compact_map_factors_coverline 59