OAI/Topology/ArtinGroups/Harmonic/ResidueActive.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.sourceCosetVector_upper_antitone_int line 14
  2. lemma OAI.HarmonicArtin.sourceCosetVector_upper_monotone_int line 26
  3. lemma OAI.HarmonicArtin.sourceResidueHeight_lt_of_ne line 38
  4. def OAI.HarmonicArtin.sourceResidueActive line 52
  5. lemma OAI.HarmonicArtin.sourceResidueActive_misses line 55
  6. abbrev OAI.HarmonicArtin.SourceResidueEarlierUpper line 68
  7. lemma OAI.HarmonicArtin.sourceResidueUpper_meets line 71
  8. lemma OAI.HarmonicArtin.sourceResidueUpper_active line 87
  9. def OAI.HarmonicArtin.sourceResidueUpperTop line 92
  10. def OAI.HarmonicArtin.sourceResidueUpperClip line 98
  11. lemma OAI.HarmonicArtin.sourceResidueUpperClip_le line 102
  12. lemma OAI.HarmonicArtin.le_sourceResidueUpperClip line 109
  13. lemma OAI.HarmonicArtin.sourceResidueUpperTop_mem line 117
  14. lemma OAI.HarmonicArtin.sourceResidueUpperClip_mem line 144
  15. def OAI.HarmonicArtin.sourceResidueUpperRetraction line 158
  16. theorem OAI.HarmonicArtin.sourceResidueEarlierUpper_contractible line 167