OAI/Topology/ArtinGroups/Harmonic/PositiveComponent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.sourcePositiveComponent line 13
  2. def OAI.HarmonicArtin.sourceClosedRegion line 16
  3. def OAI.HarmonicArtin.SourceNullSign line 19
  4. def OAI.HarmonicArtin.sourceSignAt line 24
  5. lemma OAI.HarmonicArtin.sourceSignAt_zero line 28
  6. lemma OAI.HarmonicArtin.sourceSignAt_bounds line 32
  7. lemma OAI.HarmonicArtin.sourceSignAt_level_zero line 38
  8. lemma OAI.HarmonicArtin.sourceSignAt_congr_above line 43
  9. def OAI.HarmonicArtin.sourceCosetSign line 61
  10. def OAI.HarmonicArtin.sourceSecondary line 64
  11. lemma OAI.HarmonicArtin.sourceSecondary_bounds line 67
  12. lemma OAI.HarmonicArtin.sourceCosetVector_zero_positive line 80
  13. lemma OAI.HarmonicArtin.sourceSecondary_zero line 101