OAI/Topology/ArtinGroups/Harmonic/EarlierUpper.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HarmonicArtin.SourceEarlierUpper line 10
  2. def OAI.HarmonicArtin.sourceActiveTop line 12
  3. def OAI.HarmonicArtin.sourceUpperClip line 16
  4. lemma OAI.HarmonicArtin.sourceUpperClip_le line 21
  5. lemma OAI.HarmonicArtin.le_sourceUpperClip line 26
  6. lemma OAI.HarmonicArtin.sourceUpperClip_le_top line 31
  7. lemma OAI.HarmonicArtin.sourceUpperClip_monotone line 34
  8. lemma OAI.HarmonicArtin.sourceUpperClip_mem line 38
  9. def OAI.HarmonicArtin.sourceUpperRetraction line 51
  10. lemma OAI.HarmonicArtin.sourceUpperRetraction_le line 56
  11. lemma OAI.HarmonicArtin.sourceUpperClip_idem line 59
  12. lemma OAI.HarmonicArtin.sourceUpperRetraction_idem line 64
  13. lemma OAI.HarmonicArtin.sourceActiveTop_mem line 69
  14. def OAI.HarmonicArtin.sourceUpperCenter line 83
  15. lemma OAI.HarmonicArtin.sourceUpperRetraction_le_center line 86
  16. lemma OAI.HarmonicArtin.sourceEarlierUpper_nonempty_iff line 90