OAI/Topology/ArtinGroups/Realizations/WeightLinearLinkInverse.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.weightMap_cone line 13
2. lemma OAI.HarmonicArtin.weight_support_singleton line 23
3. def OAI.HarmonicArtin.weightLinearLinkInverse line 30
4. lemma OAI.HarmonicArtin.weightLinearLinkMap_surjective line 33
5. lemma OAI.HarmonicArtin.weightLinearCone_surjective line 41
6. lemma OAI.HarmonicArtin.weightLinearCone_quotient line 52
7. def OAI.HarmonicArtin.weightLinkEmbedding line 56
8. lemma OAI.HarmonicArtin.weightCone_embedding line 62
9. lemma OAI.HarmonicArtin.continuous_comp_weightEmbedding line 78
10. theorem OAI.HarmonicArtin.continuous_of_weightParts line 88