OAI/Topology/ArtinGroups/Realizations/NoncriticalPositiveCell.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.positiveCell_same_top_type_unique line 17
  2. theorem OAI.HarmonicArtin.positiveCell_realize_top line 27
  3. abbrev OAI.HarmonicArtin.NoncriticalPositiveCell line 49
  4. def OAI.HarmonicArtin.matchingLetter line 51
  5. def OAI.HarmonicArtin.matchingOtherType line 54
  6. lemma OAI.HarmonicArtin.matchingOtherType_subset line 58
  7. lemma OAI.HarmonicArtin.matchingOtherType_spherical line 70
  8. def OAI.HarmonicArtin.positiveMatch line 79
  9. lemma OAI.HarmonicArtin.positiveMatch_top line 84
  10. lemma OAI.HarmonicArtin.positiveMatch_type line 90
  11. lemma OAI.HarmonicArtin.positiveMatch_letter line 96
  12. theorem OAI.HarmonicArtin.positiveMatch_involutive line 100
  13. theorem OAI.HarmonicArtin.positiveMatch_ne line 118
  14. theorem OAI.HarmonicArtin.positiveMatch_incident line 128
  15. theorem OAI.HarmonicArtin.spherical_positive_matching line 161