OAI/Topology/ArtinGroups/Harmonic/PositiveEarlierLinkUpper.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.positiveMatch_upper_lt line 15
2. lemma OAI.HarmonicArtin.positiveMatch_lower_lt line 22
3. lemma OAI.HarmonicArtin.positiveMatch_lower_before line 29
4. lemma OAI.HarmonicArtin.positiveMatch_symm_value line 40
5. lemma OAI.HarmonicArtin.positiveEarlier_upper_eq line 48
6. theorem OAI.HarmonicArtin.positiveEarlierLink_lower_contractible line 57
7. lemma OAI.HarmonicArtin.positiveEarlierLink_upper_iff line 82
8. def OAI.HarmonicArtin.positiveEarlierLink_upper_iso line 110