OAI/Topology/ArtinGroups/Harmonic/TypeComponent.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.framedCartan_neg_of_label_ne_two line 14
2. lemma OAI.HarmonicArtin.sourceCosetVector_positive_neighbor line 31
3. lemma OAI.HarmonicArtin.sourcePeak_neighbor line 38
4. def OAI.HarmonicArtin.sourceTypeComponent line 47
5. lemma OAI.HarmonicArtin.sourceTypeComponent_self line 52
6. lemma OAI.HarmonicArtin.sourceTypeComponent_subset line 56
7. lemma OAI.HarmonicArtin.sourceTypeComponent_peak line 59
8. lemma OAI.HarmonicArtin.sourceTypeComponent_closed line 73
9. lemma OAI.HarmonicArtin.sourceTypeComponent_commutes line 80
10. lemma OAI.HarmonicArtin.sourceTypeComponent_positiveComponent line 87
11. lemma OAI.HarmonicArtin.sourceTypeComponent_sign line 107
12. lemma OAI.HarmonicArtin.sourceBlock_above_boundary line 125
13. lemma OAI.HarmonicArtin.sourcePositiveComponent_type_neighbor line 136
14. lemma OAI.HarmonicArtin.sourcePositiveBlock_commutes line 145