OAI/Topology/ArtinGroups/ParabolicIntersections/PointedTypeComponent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Peaks and signs on connected components of a spherical closed type.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedProfile_positive_neighbor line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_neighbor line 20
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedTypeComponent_peak line 36
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedTypeComponent_positive line 51
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedTypeComponent_positiveComponent line 67
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePositiveSign_component_iff line 86
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedTypeComponent_sign line 100
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedBlock_above_boundary line 113