OAI/Topology/ArtinGroups/Harmonic/LiftedDeck.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.HarmonicArtin.liftedPartialOrder line 10
2. lemma OAI.HarmonicArtin.lifted_eq_of_le_type_eq line 14
3. lemma OAI.HarmonicArtin.lifted_lt_type line 25
4. lemma OAI.HarmonicArtin.lifted_rank_bound line 29
5. lemma OAI.HarmonicArtin.lifted_rank_strict line 32
6. lemma OAI.HarmonicArtin.liftedFace_deck_iff line 36
7. def OAI.HarmonicArtin.liftedDeck line 46
8. def OAI.HarmonicArtin.SphericalLiftedFiber line 56
9. instance OAI.HarmonicArtin.(instance at line 59) line 59