OAI/Topology/ArtinGroups/Harmonic/PrincipalOrderIso.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.principalOrderIso line 13
  2. instance OAI.HarmonicArtin.sourceRestrictionFinite line 23
  3. abbrev OAI.HarmonicArtin.SourceModelCell line 26
  4. def OAI.HarmonicArtin.sourceModelHomeomorph line 28
  5. lemma OAI.HarmonicArtin.deck_source line 34
  6. def OAI.HarmonicArtin.sourcePrincipalDeck line 37
  7. def OAI.HarmonicArtin.liftedModelHomeomorph line 42
  8. def OAI.HarmonicArtin.sourceCellMap line 46
  9. lemma OAI.HarmonicArtin.sourceCellMap_injective line 49
  10. lemma OAI.HarmonicArtin.sourceCellMap_support line 52
  11. lemma OAI.HarmonicArtin.sourceCellMap_range line 61
  12. def OAI.HarmonicArtin.sourceModelFaceMap line 68
  13. lemma OAI.HarmonicArtin.sourceModelFaceMap_included line 74
  14. lemma OAI.HarmonicArtin.sourceModelFaceMap_self line 83
  15. lemma OAI.HarmonicArtin.sourceModelFaceMap_comp line 88
  16. lemma OAI.HarmonicArtin.sourceCellMap_deck line 94
  17. lemma OAI.HarmonicArtin.sourceModelFaceMap_deck line 113