OAI/MathematicalPhysics/AlternatingFlow/BaseNames.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Effective.ratCoord line 13
  2. lemma OAI.AlternatingNS.Effective.ratCoord_computable line 15
  3. lemma OAI.AlternatingNS.Effective.ratCoord_cast line 23
  4. lemma OAI.AlternatingNS.Effective.coord_named line 27
  5. lemma OAI.AlternatingNS.Effective.cutoff_named line 33
  6. lemma OAI.AlternatingNS.Effective.direction_succ line 41
  7. lemma OAI.AlternatingNS.Effective.JetBound.spatial_d_named line 44
  8. def OAI.AlternatingNS.Effective.slotPotential line 57
  9. def OAI.AlternatingNS.Effective.loadPotential line 62
  10. lemma OAI.AlternatingNS.Effective.loadPotential_bound line 67
  11. lemma OAI.AlternatingNS.Effective.slotPotential_bound line 75
  12. lemma OAI.AlternatingNS.Effective.donor_computable line 104
  13. lemma OAI.AlternatingNS.Effective.receiver_computable line 109
  14. lemma OAI.AlternatingNS.Effective.loadPotential_named line 114
  15. lemma OAI.AlternatingNS.Effective.slotPotential_named line 128