OAI/MathematicalPhysics/AlternatingFlow/Names.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Effective.tolerance line 15
  2. lemma OAI.AlternatingNS.Effective.tolerance_cast line 17
  3. lemma OAI.AlternatingNS.Effective.tolerance_primrec line 20
  4. lemma OAI.AlternatingNS.Effective.tolerance_pos line 23
  5. lemma OAI.AlternatingNS.Effective.tolerance_tendsto line 26
  6. def OAI.AlternatingNS.Effective.Named line 30
  7. lemma OAI.AlternatingNS.Effective.computable_find line 34
  8. lemma OAI.AlternatingNS.Effective.Named.of_certificate line 46
  9. lemma OAI.AlternatingNS.Effective.Named.congr line 65
  10. lemma OAI.AlternatingNS.Effective.Named.comp line 69
  11. lemma OAI.AlternatingNS.Effective.Named.rational line 75
  12. lemma OAI.AlternatingNS.Effective.Named.const line 80
  13. lemma OAI.AlternatingNS.Effective.approximation_tendsto line 83
  14. lemma OAI.AlternatingNS.Effective.Named.add line 93
  15. lemma OAI.AlternatingNS.Effective.Named.neg line 108
  16. lemma OAI.AlternatingNS.Effective.Named.sub line 114
  17. lemma OAI.AlternatingNS.Effective.Named.mul line 118
  18. lemma OAI.AlternatingNS.Effective.Named.ite line 152
  19. lemma OAI.AlternatingNS.Effective.Named.apply_lipschitz line 161