OAI/Topology/ArtinGroups/Realizations/PositiveCellPoset.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.positiveCellToLifted_injective line 14
2. def OAI.HarmonicArtin.PositiveCellPoset line 20
3. instance OAI.HarmonicArtin.(instance at line 22) line 22
4. lemma OAI.HarmonicArtin.positiveCellPoset_le_iff line 26
5. def OAI.HarmonicArtin.positiveCellRegionIso line 29
6. lemma OAI.HarmonicArtin.topBlockMatchingKey_cases line 46
7. def OAI.HarmonicArtin.PositiveEarlier line 74
8. lemma OAI.HarmonicArtin.positiveEarlier_iff line 79
9. lemma OAI.HarmonicArtin.positiveEarlier_wf line 87
10. lemma OAI.HarmonicArtin.positiveEarlier_total line 92
11. lemma OAI.HarmonicArtin.positiveEarlier_root line 108