OAI/Topology/ArtinGroups/Harmonic/CosetVertex.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicArtin.artinParabolic_mono line 11
  2. theorem OAI.HarmonicArtin.spherical_empty line 15
  3. theorem OAI.HarmonicArtin.spherical_singleton line 19
  4. def OAI.HarmonicArtin.cosetVertex line 26
  5. theorem OAI.HarmonicArtin.rightCoset_empty line 29
  6. theorem OAI.HarmonicArtin.elementVertex_le line 34
  7. theorem OAI.HarmonicArtin.deligne_connected line 42
  8. theorem OAI.HarmonicArtin.harmonic_minimum_principle line 77
  9. theorem OAI.HarmonicArtin.harmonic_solve line 123
  10. theorem OAI.HarmonicArtin.harmonic_extension_nonneg line 130
  11. theorem OAI.HarmonicArtin.harmonic_inverse_nonneg line 137
  12. theorem OAI.HarmonicArtin.harmonic_positive_neighbor line 147
  13. theorem OAI.HarmonicArtin.harmonic_positive_path line 165
  14. theorem OAI.HarmonicArtin.harmonic_inverse_pos line 175
  15. theorem OAI.HarmonicArtin.harmonic_two_point_equality line 190
  16. theorem OAI.HarmonicArtin.harmonic_scaled_form line 212
  17. theorem OAI.HarmonicArtin.harmonic_posDef_of_strict_row line 258