OAI/Topology/ArtinGroups/Harmonic/NullPatch2.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourcePositiveComponent_boundary_zero line 15
2. lemma OAI.HarmonicArtin.sourceNullSign_image line 24
3. lemma OAI.HarmonicArtin.sourceNullSign_peak line 36
4. lemma OAI.HarmonicArtin.sourceNullSign_sign line 49
5. def OAI.HarmonicArtin.sourceNullPatch line 64
6. lemma OAI.HarmonicArtin.sourceNullPatch_nonneg line 67
7. lemma OAI.HarmonicArtin.sourceNullPatch_row line 73
8. lemma OAI.HarmonicArtin.sourcePositive_exterior line 92
9. lemma OAI.HarmonicArtin.sourcePositive_block_cap line 104
10. lemma OAI.HarmonicArtin.sourcePositive_block_values line 123