OAI/Analysis/Conductivity/Geometry/RegularPotentialCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.potentialCompletion line 12
  2. lemma OAI.ScalarConductivity.potentialCompletion_det_ne_zero line 16
  3. lemma OAI.ScalarConductivity.potentialCompletion_pairing line 31
  4. def OAI.ScalarConductivity.potentialCompletionEquiv line 37
  5. lemma OAI.ScalarConductivity.potentialCompletionEquiv_pairing line 42
  6. theorem OAI.ScalarConductivity.exists_regular_potential_coordinates line 47
  7. lemma OAI.ScalarConductivity.mem_correctionBox line 77
  8. lemma OAI.ScalarConductivity.correctionBox_isOpen line 87
  9. lemma OAI.ScalarConductivity.exists_correctionBox_inside line 90
  10. structure OAI.ScalarConductivity.RegularCorrectionBox line 103
  11. def OAI.ScalarConductivity.RegularCorrectionBox.region line 116
  12. lemma OAI.ScalarConductivity.RegularCorrectionBox.region_open line 119
  13. lemma OAI.ScalarConductivity.RegularCorrectionBox.region_target line 122
  14. lemma OAI.ScalarConductivity.RegularCorrectionBox.region_subset line 126
  15. lemma OAI.ScalarConductivity.RegularCorrectionBox.region_nonempty line 129
  16. theorem OAI.ScalarConductivity.exists_regular_correction_box line 136