OAI/Topology/ArtinGroups/Realizations/WeightCarrier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.weightEval_continuous line 14
2. instance OAI.HarmonicArtin.(instance at line 27) line 27
3. lemma OAI.HarmonicArtin.isClosed_prod_discrete_left line 33
4. lemma OAI.HarmonicArtin.orderWeights_isClosed_iff line 41
5. def OAI.HarmonicArtin.weightCarrier line 54
6. lemma OAI.HarmonicArtin.weightCarrier_finite_of_finite line 57
7. theorem OAI.HarmonicArtin.weightCarrier_finite_of_isCompact line 63