OAI/Topology/ArtinGroups/Harmonic/HarmonicExtension.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicArtin.harmonic_positive_null_alternative line 11
  2. def OAI.HarmonicArtin.harmonicExtension line 25
  3. theorem OAI.HarmonicArtin.harmonicExtension_outside line 32
  4. theorem OAI.HarmonicArtin.harmonicExtension_inside line 38
  5. theorem OAI.HarmonicArtin.harmonic_row_split line 47
  6. theorem OAI.HarmonicArtin.harmonicExtension_harmonic line 54
  7. theorem OAI.HarmonicArtin.harmonicExtension_nonneg line 70
  8. theorem OAI.HarmonicArtin.harmonic_solve_left line 90
  9. theorem OAI.HarmonicArtin.harmonicExtension_unique line 97
  10. theorem OAI.HarmonicArtin.harmonic_upper_change line 120
  11. def OAI.HarmonicArtin.framedCartan line 147
  12. theorem OAI.HarmonicArtin.framedCartan_symm line 155
  13. theorem OAI.HarmonicArtin.framedCartan_diag line 163
  14. theorem OAI.HarmonicArtin.framedCartan_off line 167
  15. theorem OAI.HarmonicArtin.framedCartan_frame line 196
  16. theorem OAI.HarmonicArtin.harmonic_lower_change line 199
  17. theorem OAI.HarmonicArtin.harmonic_boundary_comparison line 218
  18. theorem OAI.HarmonicArtin.harmonic_positive_neighbor_at line 243
  19. theorem OAI.HarmonicArtin.harmonic_support_alternative line 259